Theorem simpl22 1253

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  brbtwn2  28876  ax5seg  28909  axpasch  28912  axeuclid  28934  br8d  32581  br8  35768  cgrextend  36021  segconeq  36023  trisegint  36041  ifscgr  36057  cgrsub  36058  cgrxfr  36068  lineext  36089  seglecgr12im  36123  segletr  36127  lineunray  36160  lineelsb2  36161  cvrcmp  39301  cvlatexch3  39356  cvlsupr2  39361  atcvrj2b  39450  atexchcvrN  39458  3dim1  39485  3dim2  39486  3atlem3  39503  3atlem5  39505  lplnnle2at  39559  2llnjaN  39584  4atlem3  39614  4atlem10b  39623  4atlem12  39630  2llnma3r  39806  paddasslem4  39841  paddasslem7  39844  paddasslem8  39845  paddasslem12  39849  paddasslem13  39850  paddasslem15  39852  pmodlem1  39864  pmodlem2  39865  atmod1i1m  39876  llnexchb2lem  39886  4atex2  40095  ltrnatlw  40201  trlval4  40206  arglem1N  40208  cdlemd4  40219  cdlemd5  40220  cdleme0moN  40243  cdleme16  40303  cdleme20  40342  cdleme21k  40356  cdleme27N  40387  cdleme28c  40390  cdleme43fsv1snlem  40438  cdleme38n  40482  cdleme40n  40486  cdleme41snaw  40494  cdlemg6c  40638  cdlemg8c  40647  cdlemg8  40649  cdlemg12e  40665  cdlemg16  40675  cdlemg16ALTN  40676  cdlemg16z  40677  cdlemg16zz  40678  cdlemg18a  40696  cdlemg20  40703  cdlemg22  40705  cdlemg37  40707  cdlemg31d  40718  cdlemg33  40729  cdlemg38  40733  cdlemg44b  40750  cdlemk38  40933  cdlemk35s-id  40956  cdlemk39s-id  40958  cdlemk53b  40974  cdlemk55  40979  cdlemk35u  40982  cdlemk55u  40984  cdlemn11pre  41228