Theorem simpl23 1270

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpl23	⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒)

Proof of Theorem simpl23

Step	Hyp	Ref	Expression
1		simpl3 1210	. 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:  frrlem10  8280  mulgdirlem  19162  nosupbnd2lem1  27837  noinfbnd2lem1  27852  brbtwn2  29164  ax5seglem3a  29189  ax5seg  29197  axpasch  29200  axeuclid  29222  br8d  32865  br8  36119  cgrextend  36371  segconeq  36373  segconeu  36374  trisegint  36391  ifscgr  36407  cgrsub  36408  cgrxfr  36418  lineext  36439  seglecgr12im  36473  segletr  36477  lineunray  36510  lineelsb2  36511  cvrcmp  39919  cvlsupr2  39979  atcvrj2b  40068  atexchcvrN  40076  3atlem3  40121  3atlem5  40123  lplnnle2at  40177  lplnllnneN  40192  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  arglem1N  40826  cdlemd4  40837  cdlemd5  40838  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  cdlemg16ALTN  41294  cdlemg16zz  41296  cdlemg18a  41314  cdlemg20  41321  cdlemg22  41323  cdlemg37  41325  cdlemg31d  41336  cdlemg33  41347  cdlemg38  41351  cdlemg44b  41368  cdlemk33N  41545  cdlemk34  41546  cdlemk38  41551  cdlemk35s-id  41574  cdlemk39s-id  41576  cdlemk53b  41592  cdlemk53  41593  cdlemk55  41597  cdlemk35u  41600  cdlemk55u  41602  cdleml3N  41614  cdlemn11pre  41846  aks6d1c1  42745