Theorem simpl21 1250

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

Assertion

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

Proof of Theorem simpl21

Step	Hyp	Ref	Expression
1		simpl1 1190	. 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:  frrlem10  8181  nosupbnd2lem1  26969  noinfbnd2lem1  26984  brbtwn2  27562  ax5seglem3a  27587  ax5seg  27595  axpasch  27598  axeuclid  27620  br8d  31237  br8  34012  cgrextend  34406  segconeq  34408  trisegint  34426  ifscgr  34442  cgrsub  34443  cgrxfr  34453  lineext  34474  seglecgr12im  34508  segletr  34512  lineunray  34545  lineelsb2  34546  cvrcmp  37550  cvlatexch3  37605  cvlsupr2  37610  atexchcvrN  37708  3dim1  37735  3dim2  37736  ps-1  37745  ps-2  37746  3atlem3  37753  3atlem5  37755  lplnnle2at  37809  lplnllnneN  37824  2llnjaN  37834  4atlem3  37864  4atlem10b  37873  4atlem12  37880  2llnma3r  38056  paddasslem4  38091  paddasslem7  38094  paddasslem8  38095  paddasslem12  38099  paddasslem13  38100  pmodlem1  38114  pmodlem2  38115  llnexchb2lem  38136  4atex2  38345  ltrnatlw  38451  trlval4  38456  arglem1N  38458  cdlemd4  38469  cdlemd5  38470  cdleme0moN  38493  cdleme16  38553  cdleme20  38592  cdleme21j  38604  cdleme21k  38606  cdleme27N  38637  cdleme28c  38640  cdleme43fsv1snlem  38688  cdleme38n  38732  cdleme40n  38736  cdleme41snaw  38744  cdlemg6c  38888  cdlemg8c  38897  cdlemg8  38899  cdlemg12e  38915  cdlemg16  38925  cdlemg16ALTN  38926  cdlemg16z  38927  cdlemg16zz  38928  cdlemg18a  38946  cdlemg20  38953  cdlemg22  38955  cdlemg37  38957  cdlemg27b  38964  cdlemg31d  38968  cdlemg33  38979  cdlemg38  38983  cdlemg44b  39000  cdlemk38  39183  cdlemk35s-id  39206  cdlemk39s-id  39208  cdlemk55  39229  cdlemk35u  39232  cdlemk55u  39234  cdleml3N  39246  cdlemn11pre  39478