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

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

Proof of Theorem simpl3l
StepHypRef Expression
1 simpll 807 . 2 (((𝜑𝜓) ∧ 𝜏) → 𝜑)
213ad2antl3 1203 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:  tfisi  7223  omopth2  7833  ltmul1a  11064  xaddass  12272  xlemul2a  12312  swrdsbslen  13648  dvdsadd2b  15230  pockthg  15812  psgnunilem4  18117  efgred  18361  ptbasin  21582  basqtop  21716  xrsmopn  22816  axpasch  26020  axcontlem4  26046  elwwlks2ons3im  27074  br4  31955  nosupbnd1lem3  32162  nosupbnd1lem4  32163  btwnintr  32432  btwnexch3  32433  btwnouttr2  32435  cgrxfr  32468  lineext  32489  btwnconn1lem13  32512  btwnconn1lem14  32513  btwnconn3  32516  brsegle  32521  brsegle2  32522  segleantisym  32528  outsideofeu  32544  lineunray  32560  lineelsb2  32561  cvrcmp  35073  atcvrj2b  35221  3dimlem3  35250  3dimlem3OLDN  35251  3dim3  35258  ps-1  35266  lplnnle2at  35330  2llnm3N  35358  lvolnle3at  35371  4atlem0a  35382  4atlem3  35385  4atlem3a  35386  lnatexN  35568  paddasslem8  35616  paddasslem9  35617  paddasslem10  35618  paddasslem12  35620  paddasslem13  35621  lhp2lt  35790  lhpexle2lem  35798  lhpexle3  35801  lhpmcvr3  35814  lhpat3  35835  4atex  35865  trlval2  35953  ltrnideq  35965  ltrnatlw  35973  trlnle  35976  trlval4  35978  cdlemd4  35991  cdlemd5  35992  cdleme16  36075  cdleme21  36127  cdleme21k  36128  cdleme27cl  36156  cdleme27N  36159  cdleme29ex  36164  cdleme43fsv1snlem  36210  cdleme40m  36257  cdleme46f2g2  36283  cdleme46f2g1  36284  trlord  36359  cdlemg8  36421  cdlemg15a  36445  cdlemg16z  36449  cdlemg18a  36468  cdlemg24  36478  cdlemg38  36505  cdlemg40  36507  trlcone  36518  cdlemj2  36612  tendoid0  36615  tendoconid  36619  cdlemk34  36700  cdlemk38  36705  cdlemkid4  36724  cdlemk35s-id  36728  cdlemk39s-id  36730  cdlemk53  36747  tendospcanN  36814  cdlemm10N  36909  dihvalcqpre  37026  dihopelvalcpre  37039  dihord5b  37050  dihglblem5apreN  37082  dihmeetlem16N  37113  dihmeetlem17N  37114  dvh3dim3N  37240  qirropth  37975  mzpcong  38041  jm2.26  38071  aomclem6  38131  limcleqr  40379  fourierdlem42  40869
  Copyright terms: Public domain W3C validator