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

Theorem 3adantl2 1159
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 1141 . 2 ((𝜑𝜏𝜓) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 580 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:  3ad2antl1  1177  omord2  8182  nnmord  8247  axcc3  9848  lediv2a  11522  zdiv  12040  clatleglb  17724  mulgnn0subcl  18179  mulgsubcl  18180  ghmmulg  18308  obs2ss  20801  scmatf1  21068  neiint  21640  cnpnei  21800  caublcls  23839  axlowdimlem16  26670  clwwlkext2edg  27762  ipval2lem2  28408  fh1  29322  cm2j  29324  hoadddi  29507  hoadddir  29508  lindsadd  34766  lautco  37113  supxrge  41482  infleinflem2  41515  stoweidlem44  42206  fourierdlem41  42310  fourierdlem42  42311  fourierdlem54  42322  fourierdlem83  42351  sge0uzfsumgt  42603
  Copyright terms: Public domain W3C validator