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

Theorem 3adant3r 1363
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
3adant1l.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3adant3r ((𝜑𝜓 ∧ (𝜒𝜏)) → 𝜃)

Proof of Theorem 3adant3r
StepHypRef Expression
1 3adant1l.1 . . . 4 ((𝜑𝜓𝜒) → 𝜃)
213com13 1289 . . 3 ((𝜒𝜓𝜑) → 𝜃)
323adant1r 1359 . 2 (((𝜒𝜏) ∧ 𝜓𝜑) → 𝜃)
433com13 1289 1 ((𝜑𝜓 ∧ (𝜒𝜏)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  wfrlem12  7471  mapfien2  8355  cfeq0  9116  ltmul2  10912  lemul1  10913  lemul2  10914  lemuldiv  10941  lediv2  10951  ltdiv23  10952  lediv23  10953  dvdscmulr  15057  dvdsmulcr  15058  modremain  15179  ndvdsadd  15181  rpexp12i  15481  isdrngd  18820  cramerimp  20540  tsmsxp  22005  xblcntrps  22262  xblcntr  22263  rrxmet  23237  nvaddsub4  27640  hvmulcan2  28058  adjlnop  29073  rrnmet  33758  lfladd  34671  lflsub  34672  lshpset2N  34724  atcvrj1  35035  athgt  35060  ltrncnvel  35746  trlcnv  35770  trljat2  35772  cdlemc5  35800  trlcoabs  36326  trlcolem  36331  dicvaddcl  36796  limsupre3uzlem  40285  fourierdlem42  40684  ovnhoilem2  41137  lincext3  42570
  Copyright terms: Public domain W3C validator