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 484 . 2 ((𝜒𝜏) → 𝜒)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an3 1166 1 ((𝜑𝜓 ∧ (𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  wfrlem12OLD  8267  mapfien2  9346  cfeq0  10193  ltmul2  12007  lemul1  12008  lemul2  12009  lemuldiv  12036  lediv2  12046  ltdiv23  12047  lediv23  12048  dvdscmulr  16168  dvdsmulcr  16169  modremain  16291  ndvdsadd  16293  rpexp12i  16601  isdrngd  20215  isdrngdOLD  20217  cramerimp  22038  tsmsxp  23509  xblcntrps  23766  xblcntr  23767  rrxmet  24775  nvaddsub4  29602  hvmulcan2  30018  adjlnop  31031  rrnmet  36291  lfladd  37531  lflsub  37532  lshpset2N  37584  atcvrj1  37897  athgt  37922  ltrncnvel  38608  trlcnv  38631  trljat2  38633  cdlemc5  38661  trlcoabs  39187  trlcolem  39192  dicvaddcl  39656  limsupre3uzlem  43983  fourierdlem42  44397  ovnhoilem2  44850  lincext3  46544
  Copyright terms: Public domain W3C validator