Theorem simpl22 1250

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  brbtwn2  27176  ax5seg  27209  axpasch  27212  axeuclid  27234  br8d  30851  br8  33629  cgrextend  34237  segconeq  34239  trisegint  34257  ifscgr  34273  cgrsub  34274  cgrxfr  34284  lineext  34305  seglecgr12im  34339  segletr  34343  lineunray  34376  lineelsb2  34377  cvrcmp  37224  cvlatexch3  37279  cvlsupr2  37284  atcvrj2b  37373  atexchcvrN  37381  3dim1  37408  3dim2  37409  3atlem3  37426  3atlem5  37428  lplnnle2at  37482  2llnjaN  37507  4atlem3  37537  4atlem10b  37546  4atlem12  37553  2llnma3r  37729  paddasslem4  37764  paddasslem7  37767  paddasslem8  37768  paddasslem12  37772  paddasslem13  37773  paddasslem15  37775  pmodlem1  37787  pmodlem2  37788  atmod1i1m  37799  llnexchb2lem  37809  4atex2  38018  ltrnatlw  38124  trlval4  38129  arglem1N  38131  cdlemd4  38142  cdlemd5  38143  cdleme0moN  38166  cdleme16  38226  cdleme20  38265  cdleme21k  38279  cdleme27N  38310  cdleme28c  38313  cdleme43fsv1snlem  38361  cdleme38n  38405  cdleme40n  38409  cdleme41snaw  38417  cdlemg6c  38561  cdlemg8c  38570  cdlemg8  38572  cdlemg12e  38588  cdlemg16  38598  cdlemg16ALTN  38599  cdlemg16z  38600  cdlemg16zz  38601  cdlemg18a  38619  cdlemg20  38626  cdlemg22  38628  cdlemg37  38630  cdlemg31d  38641  cdlemg33  38652  cdlemg38  38656  cdlemg44b  38673  cdlemk38  38856  cdlemk35s-id  38879  cdlemk39s-id  38881  cdlemk53b  38897  cdlemk55  38902  cdlemk35u  38905  cdlemk55u  38907  cdlemn11pre  39151