Theorem simpl22 1265

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  brbtwn2  29050  ax5seg  29083  axpasch  29086  axeuclid  29108  br8d  32758  br8  36059  cgrextend  36311  segconeq  36313  trisegint  36331  ifscgr  36347  cgrsub  36348  cgrxfr  36358  lineext  36379  seglecgr12im  36413  segletr  36417  lineunray  36450  lineelsb2  36451  cvrcmp  39860  cvlatexch3  39915  cvlsupr2  39920  atcvrj2b  40009  atexchcvrN  40017  3dim1  40044  3dim2  40045  3atlem3  40062  3atlem5  40064  lplnnle2at  40118  2llnjaN  40143  4atlem3  40173  4atlem10b  40182  4atlem12  40189  2llnma3r  40365  paddasslem4  40400  paddasslem7  40403  paddasslem8  40404  paddasslem12  40408  paddasslem13  40409  paddasslem15  40411  pmodlem1  40423  pmodlem2  40424  atmod1i1m  40435  llnexchb2lem  40445  4atex2  40654  ltrnatlw  40760  trlval4  40765  arglem1N  40767  cdlemd4  40778  cdlemd5  40779  cdleme0moN  40802  cdleme16  40862  cdleme20  40901  cdleme21k  40915  cdleme27N  40946  cdleme28c  40949  cdleme43fsv1snlem  40997  cdleme38n  41041  cdleme40n  41045  cdleme41snaw  41053  cdlemg6c  41197  cdlemg8c  41206  cdlemg8  41208  cdlemg12e  41224  cdlemg16  41234  cdlemg16ALTN  41235  cdlemg16z  41236  cdlemg16zz  41237  cdlemg18a  41255  cdlemg20  41262  cdlemg22  41264  cdlemg37  41266  cdlemg31d  41277  cdlemg33  41288  cdlemg38  41292  cdlemg44b  41309  cdlemk38  41492  cdlemk35s-id  41515  cdlemk39s-id  41517  cdlemk53b  41533  cdlemk55  41538  cdlemk35u  41541  cdlemk55u  41543  cdlemn11pre  41787