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

Theorem 3adantl2 1208
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 1180 . 2 ((𝜑𝜏𝜓) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 575 1 (((𝜑𝜏𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  3ad2antl1  1236  omord2  7852  nnmord  7917  axcc3  9513  lediv2a  11171  zdiv  11694  clatleglb  17392  mulgnn0subcl  17821  mulgsubcl  17822  ghmmulg  17936  obs2ss  20349  scmatf1  20614  neiint  21188  cnpnei  21348  caublcls  23386  axlowdimlem16  26128  clwwlkext2edg  27306  ipval2lem2  28015  fh1  28933  cm2j  28935  hoadddi  29118  hoadddir  29119  lautco  36053  supxrge  40192  infleinflem2  40225  stoweidlem44  40898  fourierdlem41  41002  fourierdlem42  41003  fourierdlem54  41014  fourierdlem83  41043  sge0uzfsumgt  41298
  Copyright terms: Public domain W3C validator