Theorem simpl21 1252

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 1192	. 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:  frrlem10  8237  nosupbnd2lem1  27683  noinfbnd2lem1  27698  brbtwn2  28978  ax5seglem3a  29003  ax5seg  29011  axpasch  29014  axeuclid  29036  br8d  32686  br8  35950  cgrextend  36202  segconeq  36204  trisegint  36222  ifscgr  36238  cgrsub  36239  cgrxfr  36249  lineext  36270  seglecgr12im  36304  segletr  36308  lineunray  36341  lineelsb2  36342  cvrcmp  39543  cvlatexch3  39598  cvlsupr2  39603  atexchcvrN  39700  3dim1  39727  3dim2  39728  ps-1  39737  ps-2  39738  3atlem3  39745  3atlem5  39747  lplnnle2at  39801  lplnllnneN  39816  2llnjaN  39826  4atlem3  39856  4atlem10b  39865  4atlem12  39872  2llnma3r  40048  paddasslem4  40083  paddasslem7  40086  paddasslem8  40087  paddasslem12  40091  paddasslem13  40092  pmodlem1  40106  pmodlem2  40107  llnexchb2lem  40128  4atex2  40337  ltrnatlw  40443  trlval4  40448  arglem1N  40450  cdlemd4  40461  cdlemd5  40462  cdleme0moN  40485  cdleme16  40545  cdleme20  40584  cdleme21j  40596  cdleme21k  40598  cdleme27N  40629  cdleme28c  40632  cdleme43fsv1snlem  40680  cdleme38n  40724  cdleme40n  40728  cdleme41snaw  40736  cdlemg6c  40880  cdlemg8c  40889  cdlemg8  40891  cdlemg12e  40907  cdlemg16  40917  cdlemg16ALTN  40918  cdlemg16z  40919  cdlemg16zz  40920  cdlemg18a  40938  cdlemg20  40945  cdlemg22  40947  cdlemg37  40949  cdlemg27b  40956  cdlemg31d  40960  cdlemg33  40971  cdlemg38  40975  cdlemg44b  40992  cdlemk38  41175  cdlemk35s-id  41198  cdlemk39s-id  41200  cdlemk55  41221  cdlemk35u  41224  cdlemk55u  41226  cdleml3N  41238  cdlemn11pre  41470