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

Theorem simpl21 1320
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
StepHypRef Expression
1 simpl1 1227 . 2 (((𝜑𝜓𝜒) ∧ 𝜂) → 𝜑)
213ad2antl2 1201 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  brbtwn2  26007  ax5seglem3a  26032  ax5seg  26040  axpasch  26043  axeuclid  26065  br8d  29761  br8  31985  nosupbnd2lem1  32199  cgrextend  32453  segconeq  32455  trisegint  32473  ifscgr  32489  cgrsub  32490  cgrxfr  32500  lineext  32521  seglecgr12im  32555  segletr  32559  lineunray  32592  lineelsb2  32593  cvrcmp  35093  cvlatexch3  35148  cvlsupr2  35153  atexchcvrN  35249  3dim1  35276  3dim2  35277  ps-1  35286  ps-2  35287  3atlem3  35294  3atlem5  35296  lplnnle2at  35350  lplnllnneN  35365  2llnjaN  35375  4atlem3  35405  4atlem10b  35414  4atlem12  35421  2llnma3r  35597  paddasslem4  35632  paddasslem7  35635  paddasslem8  35636  paddasslem12  35640  paddasslem13  35641  pmodlem1  35655  pmodlem2  35656  llnexchb2lem  35677  4atex2  35886  ltrnatlw  35993  trlval4  35998  arglem1N  36000  cdlemd4  36011  cdlemd5  36012  cdleme0moN  36035  cdleme16  36095  cdleme20  36134  cdleme21j  36146  cdleme21k  36148  cdleme27N  36179  cdleme28c  36182  cdleme43fsv1snlem  36230  cdleme38n  36274  cdleme40n  36278  cdleme41snaw  36286  cdlemg6c  36430  cdlemg8c  36439  cdlemg8  36441  cdlemg12e  36457  cdlemg16  36467  cdlemg16ALTN  36468  cdlemg16z  36469  cdlemg16zz  36470  cdlemg18a  36488  cdlemg20  36495  cdlemg22  36497  cdlemg37  36499  cdlemg27b  36506  cdlemg31d  36510  cdlemg33  36521  cdlemg38  36525  cdlemg44b  36542  cdlemk38  36725  cdlemk35s-id  36748  cdlemk39s-id  36750  cdlemk55  36771  cdlemk35u  36774  cdlemk55u  36776  cdleml3N  36788  cdlemn11pre  37021
  Copyright terms: Public domain W3C validator