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

Theorem 3adantl2 1168
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 1150 . 2 ((𝜑𝜏𝜓) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 581 1 (((𝜑𝜏𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  3ad2antl1  1186  omord2  8518  nnmord  8583  axcc3  10382  lediv2a  12057  zdiv  12581  clatleglb  18415  mulgnn0subcl  18897  mulgsubcl  18898  ghmmulg  19028  obs2ss  21158  scmatf1  21903  neiint  22478  cnpnei  22638  caublcls  24696  axlowdimlem16  27955  clwwlkext2edg  29049  ipval2lem2  29695  fh1  30609  cm2j  30611  hoadddi  30794  hoadddir  30795  lindsadd  36121  lautco  38610  sticksstones1  40604  sticksstones12  40616  supxrge  43663  infleinflem2  43696  stoweidlem44  44375  fourierdlem41  44479  fourierdlem42  44480  fourierdlem54  44491  fourierdlem83  44520  sge0uzfsumgt  44775
  Copyright terms: Public domain W3C validator