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

Theorem 3adantl2 1164
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
Hypothesis
Ref Expression
3adantl.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
3adantl2 (((𝜑𝜏𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem 3adantl2
StepHypRef Expression
1 3simpb 1146 . 2 ((𝜑𝜏𝜓) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 579 1 (((𝜑𝜏𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1084
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 396  df-3an 1086
This theorem is referenced by:  3ad2antl1  1182  omord2  8568  nnmord  8633  axcc3  10435  lediv2a  12112  zdiv  12636  clatleglb  18483  mulgnn0subcl  19014  mulgsubcl  19015  ghmmulg  19153  obs2ss  21624  scmatf1  22388  neiint  22963  cnpnei  23123  caublcls  25192  axlowdimlem16  28723  clwwlkext2edg  29818  ipval2lem2  30466  fh1  31380  cm2j  31382  hoadddi  31565  hoadddir  31566  lindsadd  36994  lautco  39481  sticksstones1  41523  sticksstones12  41535  supxrge  44620  infleinflem2  44653  stoweidlem44  45332  fourierdlem41  45436  fourierdlem42  45437  fourierdlem54  45448  fourierdlem83  45477  sge0uzfsumgt  45732
  Copyright terms: Public domain W3C validator