Theorem simpl22 1259

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

Assertion

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

Proof of Theorem simpl22

Step	Hyp	Ref	Expression
1		simpl2 1199	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl2 1193	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  brbtwn2  28999  ax5seg  29032  axpasch  29035  axeuclid  29057  br8d  32707  br8  35985  cgrextend  36237  segconeq  36239  trisegint  36257  ifscgr  36273  cgrsub  36274  cgrxfr  36284  lineext  36305  seglecgr12im  36339  segletr  36343  lineunray  36376  lineelsb2  36377  cvrcmp  39776  cvlatexch3  39831  cvlsupr2  39836  atcvrj2b  39925  atexchcvrN  39933  3dim1  39960  3dim2  39961  3atlem3  39978  3atlem5  39980  lplnnle2at  40034  2llnjaN  40059  4atlem3  40089  4atlem10b  40098  4atlem12  40105  2llnma3r  40281  paddasslem4  40316  paddasslem7  40319  paddasslem8  40320  paddasslem12  40324  paddasslem13  40325  paddasslem15  40327  pmodlem1  40339  pmodlem2  40340  atmod1i1m  40351  llnexchb2lem  40361  4atex2  40570  ltrnatlw  40676  trlval4  40681  arglem1N  40683  cdlemd4  40694  cdlemd5  40695  cdleme0moN  40718  cdleme16  40778  cdleme20  40817  cdleme21k  40831  cdleme27N  40862  cdleme28c  40865  cdleme43fsv1snlem  40913  cdleme38n  40957  cdleme40n  40961  cdleme41snaw  40969  cdlemg6c  41113  cdlemg8c  41122  cdlemg8  41124  cdlemg12e  41140  cdlemg16  41150  cdlemg16ALTN  41151  cdlemg16z  41152  cdlemg16zz  41153  cdlemg18a  41171  cdlemg20  41178  cdlemg22  41180  cdlemg37  41182  cdlemg31d  41193  cdlemg33  41204  cdlemg38  41208  cdlemg44b  41225  cdlemk38  41408  cdlemk35s-id  41431  cdlemk39s-id  41433  cdlemk53b  41449  cdlemk55  41454  cdlemk35u  41457  cdlemk55u  41459  cdlemn11pre  41703