MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpl23 Structured version   Visualization version   GIF version

Theorem simpl23 1250
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
StepHypRef Expression
1 simpl3 1190 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜒)
213ad2antl2 1183 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 400  df-3an 1086
This theorem is referenced by:  mulgdirlem  18260  brbtwn2  26708  ax5seglem3a  26733  ax5seg  26741  axpasch  26744  axeuclid  26766  br8d  30380  br8  33077  frrlem10  33217  nosupbnd2lem1  33300  cgrextend  33554  segconeq  33556  segconeu  33557  trisegint  33574  ifscgr  33590  cgrsub  33591  cgrxfr  33601  lineext  33622  seglecgr12im  33656  segletr  33660  lineunray  33693  lineelsb2  33694  cvrcmp  36551  cvlsupr2  36611  atcvrj2b  36700  atexchcvrN  36708  3atlem3  36753  3atlem5  36755  lplnnle2at  36809  lplnllnneN  36824  4atlem3  36864  4atlem10b  36873  4atlem12  36880  2llnma3r  37056  paddasslem4  37091  paddasslem7  37094  paddasslem8  37095  paddasslem12  37099  paddasslem13  37100  paddasslem15  37102  pmodlem1  37114  pmodlem2  37115  atmod1i1m  37126  llnexchb2lem  37136  4atex2  37345  ltrnatlw  37451  arglem1N  37458  cdlemd4  37469  cdlemd5  37470  cdleme16  37553  cdleme20  37592  cdleme21k  37606  cdleme27N  37637  cdleme28c  37640  cdleme43fsv1snlem  37688  cdleme38n  37732  cdleme40n  37736  cdleme41snaw  37744  cdlemg6c  37888  cdlemg8c  37897  cdlemg8  37899  cdlemg12e  37915  cdlemg16ALTN  37926  cdlemg16zz  37928  cdlemg18a  37946  cdlemg20  37953  cdlemg22  37955  cdlemg37  37957  cdlemg31d  37968  cdlemg33  37979  cdlemg38  37983  cdlemg44b  38000  cdlemk33N  38177  cdlemk34  38178  cdlemk38  38183  cdlemk35s-id  38206  cdlemk39s-id  38208  cdlemk53b  38224  cdlemk53  38225  cdlemk55  38229  cdlemk35u  38232  cdlemk55u  38234  cdleml3N  38246  cdlemn11pre  38478
  Copyright terms: Public domain W3C validator