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

Theorem 3adant3r 1173
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 483 . 2 ((𝜒𝜏) → 𝜒)
2 ad4ant3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
31, 2syl3an3 1157 1 ((𝜑𝜓 ∧ (𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  wfrlem12  7955  mapfien2  8860  cfeq0  9666  ltmul2  11479  lemul1  11480  lemul2  11481  lemuldiv  11508  lediv2  11518  ltdiv23  11519  lediv23  11520  dvdscmulr  15626  dvdsmulcr  15627  modremain  15747  ndvdsadd  15749  rpexp12i  16054  isdrngd  19456  cramerimp  21223  tsmsxp  22690  xblcntrps  22947  xblcntr  22948  rrxmet  23938  nvaddsub4  28361  hvmulcan2  28777  adjlnop  29790  rrnmet  34988  lfladd  36082  lflsub  36083  lshpset2N  36135  atcvrj1  36447  athgt  36472  ltrncnvel  37158  trlcnv  37181  trljat2  37183  cdlemc5  37211  trlcoabs  37737  trlcolem  37742  dicvaddcl  38206  limsupre3uzlem  41892  fourierdlem42  42311  ovnhoilem2  42761  lincext3  44439
  Copyright terms: Public domain W3C validator