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

Theorem 3adantl2 1167
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 1149 . 2 ((𝜑𝜏𝜓) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 580 1 (((𝜑𝜏𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 397  df-3an 1089
This theorem is referenced by:  3ad2antl1  1185  omord2  8513  nnmord  8578  axcc3  10373  lediv2a  12048  zdiv  12572  clatleglb  18406  mulgnn0subcl  18887  mulgsubcl  18888  ghmmulg  19018  obs2ss  21133  scmatf1  21878  neiint  22453  cnpnei  22613  caublcls  24671  axlowdimlem16  27904  clwwlkext2edg  28998  ipval2lem2  29644  fh1  30558  cm2j  30560  hoadddi  30743  hoadddir  30744  lindsadd  36062  lautco  38551  sticksstones1  40545  sticksstones12  40557  supxrge  43548  infleinflem2  43581  stoweidlem44  44257  fourierdlem41  44361  fourierdlem42  44362  fourierdlem54  44373  fourierdlem83  44402  sge0uzfsumgt  44657
  Copyright terms: Public domain W3C validator