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

Theorem simpl22 1323
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)
Assertion
Ref Expression
simpl22 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem simpl22
StepHypRef Expression
1 simpl2 1230 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜓)
213ad2antl2 1202 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  brbtwn2  25984  ax5seg  26017  axpasch  26020  axeuclid  26042  br8d  29729  br8  31953  cgrextend  32421  segconeq  32423  trisegint  32441  ifscgr  32457  cgrsub  32458  cgrxfr  32468  lineext  32489  seglecgr12im  32523  segletr  32527  lineunray  32560  lineelsb2  32561  cvrcmp  35073  cvlatexch3  35128  cvlsupr2  35133  atcvrj2b  35221  atexchcvrN  35229  3dim1  35256  3dim2  35257  3atlem3  35274  3atlem5  35276  lplnnle2at  35330  2llnjaN  35355  4atlem3  35385  4atlem10b  35394  4atlem12  35401  2llnma3r  35577  paddasslem4  35612  paddasslem7  35615  paddasslem8  35616  paddasslem12  35620  paddasslem13  35621  paddasslem15  35623  pmodlem1  35635  pmodlem2  35636  atmod1i1m  35647  llnexchb2lem  35657  4atex2  35866  ltrnatlw  35973  trlval4  35978  arglem1N  35980  cdlemd4  35991  cdlemd5  35992  cdleme0moN  36015  cdleme16  36075  cdleme20  36114  cdleme21k  36128  cdleme27N  36159  cdleme28c  36162  cdleme43fsv1snlem  36210  cdleme38n  36254  cdleme40n  36258  cdleme41snaw  36266  cdlemg6c  36410  cdlemg8c  36419  cdlemg8  36421  cdlemg12e  36437  cdlemg16  36447  cdlemg16ALTN  36448  cdlemg16z  36449  cdlemg16zz  36450  cdlemg18a  36468  cdlemg20  36475  cdlemg22  36477  cdlemg37  36479  cdlemg31d  36490  cdlemg33  36501  cdlemg38  36505  cdlemg44b  36522  cdlemk38  36705  cdlemk35s-id  36728  cdlemk39s-id  36730  cdlemk53b  36746  cdlemk55  36751  cdlemk35u  36754  cdlemk55u  36756  cdlemn11pre  37001
  Copyright terms: Public domain W3C validator