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

Theorem 3adantl2 1160
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 1142 . 2 ((𝜑𝜏𝜓) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 580 1 (((𝜑𝜏𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1080
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 1082
This theorem is referenced by:  3ad2antl1  1178  omord2  8050  nnmord  8115  axcc3  9713  lediv2a  11388  zdiv  11906  clatleglb  17569  mulgnn0subcl  18000  mulgsubcl  18001  ghmmulg  18115  obs2ss  20559  scmatf1  20828  neiint  21400  cnpnei  21560  caublcls  23599  axlowdimlem16  26430  clwwlkext2edg  27521  ipval2lem2  28168  fh1  29082  cm2j  29084  hoadddi  29267  hoadddir  29268  lindsadd  34437  lautco  36785  supxrge  41168  infleinflem2  41201  stoweidlem44  41893  fourierdlem41  41997  fourierdlem42  41998  fourierdlem54  42009  fourierdlem83  42038  sge0uzfsumgt  42290
  Copyright terms: Public domain W3C validator