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

Theorem 3adant3r 1182
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)
Hypothesis
Ref Expression
ad4ant3.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3adant3r ((𝜑𝜓 ∧ (𝜒𝜏)) → 𝜃)

Proof of Theorem 3adant3r
StepHypRef Expression
1 simpl 482 . 2 ((𝜒𝜏) → 𝜒)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an3 1166 1 ((𝜑𝜓 ∧ (𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087
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 207  df-an 396  df-3an 1089
This theorem is referenced by:  wfrlem12OLD  8360  mapfien2  9449  cfeq0  10296  ltmul2  12118  lemul1  12119  lemul2  12120  lemuldiv  12148  lediv2  12158  ltdiv23  12159  lediv23  12160  dvdscmulr  16322  dvdsmulcr  16323  modremain  16445  ndvdsadd  16447  rpexp12i  16761  isdrngd  20765  isdrngdOLD  20767  cramerimp  22692  tsmsxp  24163  xblcntrps  24420  xblcntr  24421  rrxmet  25442  nvaddsub4  30676  hvmulcan2  31092  adjlnop  32105  rrnmet  37836  lfladd  39067  lflsub  39068  lshpset2N  39120  atcvrj1  39433  athgt  39458  ltrncnvel  40144  trlcnv  40167  trljat2  40169  cdlemc5  40197  trlcoabs  40723  trlcolem  40728  dicvaddcl  41192  limsupre3uzlem  45750  fourierdlem42  46164  ovnhoilem2  46617  lincext3  48373
  Copyright terms: Public domain W3C validator