Theorem simpl22 1245

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 1185	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl2 1179	1 ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓)

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

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 1082

This theorem is referenced by:  brbtwn2  26378  ax5seg  26411  axpasch  26414  axeuclid  26436  br8d  30047  br8  32602  cgrextend  33080  segconeq  33082  trisegint  33100  ifscgr  33116  cgrsub  33117  cgrxfr  33127  lineext  33148  seglecgr12im  33182  segletr  33186  lineunray  33219  lineelsb2  33220  cvrcmp  35971  cvlatexch3  36026  cvlsupr2  36031  atcvrj2b  36120  atexchcvrN  36128  3dim1  36155  3dim2  36156  3atlem3  36173  3atlem5  36175  lplnnle2at  36229  2llnjaN  36254  4atlem3  36284  4atlem10b  36293  4atlem12  36300  2llnma3r  36476  paddasslem4  36511  paddasslem7  36514  paddasslem8  36515  paddasslem12  36519  paddasslem13  36520  paddasslem15  36522  pmodlem1  36534  pmodlem2  36535  atmod1i1m  36546  llnexchb2lem  36556  4atex2  36765  ltrnatlw  36871  trlval4  36876  arglem1N  36878  cdlemd4  36889  cdlemd5  36890  cdleme0moN  36913  cdleme16  36973  cdleme20  37012  cdleme21k  37026  cdleme27N  37057  cdleme28c  37060  cdleme43fsv1snlem  37108  cdleme38n  37152  cdleme40n  37156  cdleme41snaw  37164  cdlemg6c  37308  cdlemg8c  37317  cdlemg8  37319  cdlemg12e  37335  cdlemg16  37345  cdlemg16ALTN  37346  cdlemg16z  37347  cdlemg16zz  37348  cdlemg18a  37366  cdlemg20  37373  cdlemg22  37375  cdlemg37  37377  cdlemg31d  37388  cdlemg33  37399  cdlemg38  37403  cdlemg44b  37420  cdlemk38  37603  cdlemk35s-id  37626  cdlemk39s-id  37628  cdlemk53b  37644  cdlemk55  37649  cdlemk35u  37652  cdlemk55u  37654  cdlemn11pre  37898