Theorem simpl23 1325

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpl23	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒)

Proof of Theorem simpl23

Step	Hyp	Ref	Expression
1		simpl3 1232	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl2 1202	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1074

This theorem is referenced by:  mulgdirlem  17773  brbtwn2  25984  ax5seglem3a  26009  ax5seg  26017  axpasch  26020  axeuclid  26042  br8d  29729  br8  31953  nosupbnd2lem1  32167  cgrextend  32421  segconeq  32423  segconeu  32424  trisegint  32441  ifscgr  32457  cgrsub  32458  cgrxfr  32468  lineext  32489  seglecgr12im  32523  segletr  32527  lineunray  32560  lineelsb2  32561  cvrcmp  35073  cvlsupr2  35133  atcvrj2b  35221  atexchcvrN  35229  3atlem3  35274  3atlem5  35276  lplnnle2at  35330  lplnllnneN  35345  4atlem3  35385  4atlem10b  35394  4atlem12  35401  2llnma3r  35577  paddasslem4  35612  paddasslem7  35615  paddasslem8  35616  paddasslem12  35620  paddasslem13  35621  paddasslem15  35623  pmodlem1  35635  pmodlem2  35636  atmod1i1m  35647  llnexchb2lem  35657  4atex2  35866  ltrnatlw  35973  arglem1N  35980  cdlemd4  35991  cdlemd5  35992  cdleme16  36075  cdleme20  36114  cdleme21k  36128  cdleme27N  36159  cdleme28c  36162  cdleme43fsv1snlem  36210  cdleme38n  36254  cdleme40n  36258  cdleme41snaw  36266  cdlemg6c  36410  cdlemg8c  36419  cdlemg8  36421  cdlemg12e  36437  cdlemg16ALTN  36448  cdlemg16zz  36450  cdlemg18a  36468  cdlemg20  36475  cdlemg22  36477  cdlemg37  36479  cdlemg31d  36490  cdlemg33  36501  cdlemg38  36505  cdlemg44b  36522  cdlemk33N  36699  cdlemk34  36700  cdlemk38  36705  cdlemk35s-id  36728  cdlemk39s-id  36730  cdlemk53b  36746  cdlemk53  36747  cdlemk55  36751  cdlemk35u  36754  cdlemk55u  36756  cdleml3N  36768  cdlemn11pre  37001