Theorem simpl23 1254

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  frrlem10  8320  mulgdirlem  19123  nosupbnd2lem1  27760  noinfbnd2lem1  27775  brbtwn2  28920  ax5seglem3a  28945  ax5seg  28953  axpasch  28956  axeuclid  28978  br8d  32622  br8  35756  cgrextend  36009  segconeq  36011  segconeu  36012  trisegint  36029  ifscgr  36045  cgrsub  36046  cgrxfr  36056  lineext  36077  seglecgr12im  36111  segletr  36115  lineunray  36148  lineelsb2  36149  cvrcmp  39284  cvlsupr2  39344  atcvrj2b  39434  atexchcvrN  39442  3atlem3  39487  3atlem5  39489  lplnnle2at  39543  lplnllnneN  39558  4atlem3  39598  4atlem10b  39607  4atlem12  39614  2llnma3r  39790  paddasslem4  39825  paddasslem7  39828  paddasslem8  39829  paddasslem12  39833  paddasslem13  39834  paddasslem15  39836  pmodlem1  39848  pmodlem2  39849  atmod1i1m  39860  llnexchb2lem  39870  4atex2  40079  ltrnatlw  40185  arglem1N  40192  cdlemd4  40203  cdlemd5  40204  cdleme16  40287  cdleme20  40326  cdleme21k  40340  cdleme27N  40371  cdleme28c  40374  cdleme43fsv1snlem  40422  cdleme38n  40466  cdleme40n  40470  cdleme41snaw  40478  cdlemg6c  40622  cdlemg8c  40631  cdlemg8  40633  cdlemg12e  40649  cdlemg16ALTN  40660  cdlemg16zz  40662  cdlemg18a  40680  cdlemg20  40687  cdlemg22  40689  cdlemg37  40691  cdlemg31d  40702  cdlemg33  40713  cdlemg38  40717  cdlemg44b  40734  cdlemk33N  40911  cdlemk34  40912  cdlemk38  40917  cdlemk35s-id  40940  cdlemk39s-id  40942  cdlemk53b  40958  cdlemk53  40959  cdlemk55  40963  cdlemk35u  40966  cdlemk55u  40968  cdleml3N  40980  cdlemn11pre  41212  aks6d1c1  42117