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

Theorem 3adant3r 1195
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 468 . 2 ((𝜒𝜏) → 𝜒)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an3 1169 1 ((𝜑𝜓 ∧ (𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  wfrlem12  7579  mapfien2  8470  cfeq0  9280  ltmul2  11076  lemul1  11077  lemul2  11078  lemuldiv  11105  lediv2  11115  ltdiv23  11116  lediv23  11117  dvdscmulr  15219  dvdsmulcr  15220  modremain  15340  ndvdsadd  15342  rpexp12i  15641  isdrngd  18982  cramerimp  20712  tsmsxp  22178  xblcntrps  22435  xblcntr  22436  rrxmet  23410  nvaddsub4  27852  hvmulcan2  28270  adjlnop  29285  rrnmet  33960  lfladd  34875  lflsub  34876  lshpset2N  34928  atcvrj1  35239  athgt  35264  ltrncnvel  35950  trlcnv  35974  trljat2  35976  cdlemc5  36004  trlcoabs  36530  trlcolem  36535  dicvaddcl  37000  limsupre3uzlem  40485  fourierdlem42  40883  ovnhoilem2  41336  lincext3  42773
  Copyright terms: Public domain W3C validator