Theorem simpl22 1269

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  brbtwn2  29164  ax5seg  29197  axpasch  29200  axeuclid  29222  br8d  32865  br8  36119  cgrextend  36371  segconeq  36373  trisegint  36391  ifscgr  36407  cgrsub  36408  cgrxfr  36418  lineext  36439  seglecgr12im  36473  segletr  36477  lineunray  36510  lineelsb2  36511  cvrcmp  39919  cvlatexch3  39974  cvlsupr2  39979  atcvrj2b  40068  atexchcvrN  40076  3dim1  40103  3dim2  40104  3atlem3  40121  3atlem5  40123  lplnnle2at  40177  2llnjaN  40202  4atlem3  40232  4atlem10b  40241  4atlem12  40248  2llnma3r  40424  paddasslem4  40459  paddasslem7  40462  paddasslem8  40463  paddasslem12  40467  paddasslem13  40468  paddasslem15  40470  pmodlem1  40482  pmodlem2  40483  atmod1i1m  40494  llnexchb2lem  40504  4atex2  40713  ltrnatlw  40819  trlval4  40824  arglem1N  40826  cdlemd4  40837  cdlemd5  40838  cdleme0moN  40861  cdleme16  40921  cdleme20  40960  cdleme21k  40974  cdleme27N  41005  cdleme28c  41008  cdleme43fsv1snlem  41056  cdleme38n  41100  cdleme40n  41104  cdleme41snaw  41112  cdlemg6c  41256  cdlemg8c  41265  cdlemg8  41267  cdlemg12e  41283  cdlemg16  41293  cdlemg16ALTN  41294  cdlemg16z  41295  cdlemg16zz  41296  cdlemg18a  41314  cdlemg20  41321  cdlemg22  41323  cdlemg37  41325  cdlemg31d  41336  cdlemg33  41347  cdlemg38  41351  cdlemg44b  41368  cdlemk38  41551  cdlemk35s-id  41574  cdlemk39s-id  41576  cdlemk53b  41592  cdlemk55  41597  cdlemk35u  41600  cdlemk55u  41602  cdlemn11pre  41846