Theorem simpl21 1249

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  frrlem10  8282  nosupbnd2lem1  27454  noinfbnd2lem1  27469  brbtwn2  28430  ax5seglem3a  28455  ax5seg  28463  axpasch  28466  axeuclid  28488  br8d  32106  br8  35030  cgrextend  35284  segconeq  35286  trisegint  35304  ifscgr  35320  cgrsub  35321  cgrxfr  35331  lineext  35352  seglecgr12im  35386  segletr  35390  lineunray  35423  lineelsb2  35424  cvrcmp  38456  cvlatexch3  38511  cvlsupr2  38516  atexchcvrN  38614  3dim1  38641  3dim2  38642  ps-1  38651  ps-2  38652  3atlem3  38659  3atlem5  38661  lplnnle2at  38715  lplnllnneN  38730  2llnjaN  38740  4atlem3  38770  4atlem10b  38779  4atlem12  38786  2llnma3r  38962  paddasslem4  38997  paddasslem7  39000  paddasslem8  39001  paddasslem12  39005  paddasslem13  39006  pmodlem1  39020  pmodlem2  39021  llnexchb2lem  39042  4atex2  39251  ltrnatlw  39357  trlval4  39362  arglem1N  39364  cdlemd4  39375  cdlemd5  39376  cdleme0moN  39399  cdleme16  39459  cdleme20  39498  cdleme21j  39510  cdleme21k  39512  cdleme27N  39543  cdleme28c  39546  cdleme43fsv1snlem  39594  cdleme38n  39638  cdleme40n  39642  cdleme41snaw  39650  cdlemg6c  39794  cdlemg8c  39803  cdlemg8  39805  cdlemg12e  39821  cdlemg16  39831  cdlemg16ALTN  39832  cdlemg16z  39833  cdlemg16zz  39834  cdlemg18a  39852  cdlemg20  39859  cdlemg22  39861  cdlemg37  39863  cdlemg27b  39870  cdlemg31d  39874  cdlemg33  39885  cdlemg38  39889  cdlemg44b  39906  cdlemk38  40089  cdlemk35s-id  40112  cdlemk39s-id  40114  cdlemk55  40135  cdlemk35u  40138  cdlemk55u  40140  cdleml3N  40152  cdlemn11pre  40384