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

Theorem adantlrr 752
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
Hypothesis
Ref Expression
adantl2.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
adantlrr (((𝜑 ∧ (𝜓𝜏)) ∧ 𝜒) → 𝜃)

Proof of Theorem adantlrr
StepHypRef Expression
1 simpl 471 . 2 ((𝜓𝜏) → 𝜓)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl2 680 1 (((𝜑 ∧ (𝜓𝜏)) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  disjxiun  4573  oelim  7478  odi  7523  marypha1lem  8199  dfac12lem2  8826  infunsdom  8896  isf34lem4  9059  distrlem1pr  9703  lcmgcdlem  15103  lcmdvds  15105  drsdirfi  16707  isacs3lem  16935  conjnmzb  17464  psgndif  19712  frlmsslsp  19896  metss2lem  22067  nghmcn  22291  bndth  22496  itg2monolem1  23240  dvmptfsum  23459  ply1divex  23617  itgulm  23883  rpvmasumlem  24893  dchrmusum2  24900  dchrisum0lem2  24924  dchrisum0lem3  24925  mulog2sumlem2  24941  pntibndlem3  24998  3v3e3cycl1  25938  4cycl4v4e  25960  blocni  26850  superpos  28403  chirredlem2  28440  eulerpartlemgvv  29571  ballotlemfc0  29687  ballotlemfcc  29688  bj-finsumval0  32127  fin2solem  32368  matunitlindflem1  32378  poimirlem28  32410  heicant  32417  ftc1anclem6  32463  ftc1anc  32466  fdc  32514  incsequz  32517  ismtyres  32580  isdrngo2  32730  rngohomco  32746  keridl  32804  linepsubN  33859  pmapsub  33875  mzpcompact2lem  36135  pellex  36220  monotuz  36327  unxpwdom3  36486  dssmapnvod  37137  radcnvrat  37338  fprodexp  38465  fprodabs2  38466  dvnprodlem1  38640  stoweidlem34  38731  fourierdlem42  38846  elaa2  38931  sge0iunmptlemfi  39110  wwlksubclwwlks  41234  aacllem  42319
  Copyright terms: Public domain W3C validator