Theorem simpl22 1251

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

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

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

This theorem is referenced by:  brbtwn2  27282  ax5seg  27315  axpasch  27318  axeuclid  27340  br8d  30959  br8  33732  cgrextend  34319  segconeq  34321  trisegint  34339  ifscgr  34355  cgrsub  34356  cgrxfr  34366  lineext  34387  seglecgr12im  34421  segletr  34425  lineunray  34458  lineelsb2  34459  cvrcmp  37304  cvlatexch3  37359  cvlsupr2  37364  atcvrj2b  37453  atexchcvrN  37461  3dim1  37488  3dim2  37489  3atlem3  37506  3atlem5  37508  lplnnle2at  37562  2llnjaN  37587  4atlem3  37617  4atlem10b  37626  4atlem12  37633  2llnma3r  37809  paddasslem4  37844  paddasslem7  37847  paddasslem8  37848  paddasslem12  37852  paddasslem13  37853  paddasslem15  37855  pmodlem1  37867  pmodlem2  37868  atmod1i1m  37879  llnexchb2lem  37889  4atex2  38098  ltrnatlw  38204  trlval4  38209  arglem1N  38211  cdlemd4  38222  cdlemd5  38223  cdleme0moN  38246  cdleme16  38306  cdleme20  38345  cdleme21k  38359  cdleme27N  38390  cdleme28c  38393  cdleme43fsv1snlem  38441  cdleme38n  38485  cdleme40n  38489  cdleme41snaw  38497  cdlemg6c  38641  cdlemg8c  38650  cdlemg8  38652  cdlemg12e  38668  cdlemg16  38678  cdlemg16ALTN  38679  cdlemg16z  38680  cdlemg16zz  38681  cdlemg18a  38699  cdlemg20  38706  cdlemg22  38708  cdlemg37  38710  cdlemg31d  38721  cdlemg33  38732  cdlemg38  38736  cdlemg44b  38753  cdlemk38  38936  cdlemk35s-id  38959  cdlemk39s-id  38961  cdlemk53b  38977  cdlemk55  38982  cdlemk35u  38985  cdlemk55u  38987  cdlemn11pre  39231