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

Theorem 3adant3r 1177
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 485 . 2 ((𝜒𝜏) → 𝜒)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an3 1161 1 ((𝜑𝜓 ∧ (𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1083
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 209  df-an 399  df-3an 1085
This theorem is referenced by:  wfrlem12  7944  mapfien2  8850  cfeq0  9656  ltmul2  11469  lemul1  11470  lemul2  11471  lemuldiv  11498  lediv2  11508  ltdiv23  11509  lediv23  11510  dvdscmulr  15618  dvdsmulcr  15619  modremain  15737  ndvdsadd  15739  rpexp12i  16044  isdrngd  19503  cramerimp  21271  tsmsxp  22739  xblcntrps  22996  xblcntr  22997  rrxmet  23991  nvaddsub4  28419  hvmulcan2  28835  adjlnop  29848  rrnmet  35143  lfladd  36238  lflsub  36239  lshpset2N  36291  atcvrj1  36603  athgt  36628  ltrncnvel  37314  trlcnv  37337  trljat2  37339  cdlemc5  37367  trlcoabs  37893  trlcolem  37898  dicvaddcl  38362  limsupre3uzlem  42168  fourierdlem42  42582  ovnhoilem2  43032  lincext3  44656
  Copyright terms: Public domain W3C validator