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

Theorem 3adantl1 1168
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
Hypothesis
Ref Expression
3adantl.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
3adantl1 (((𝜏𝜑𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem 3adantl1
StepHypRef Expression
1 3simpc 1143 . 2 ((𝜏𝜑𝜓) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 575 1 (((𝜏𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1071
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 199  df-an 387  df-3an 1073
This theorem is referenced by:  3ad2antl2  1194  3ad2antl3  1195  funcnvqp  6198  onfununi  7721  omord2  7931  en2eqpr  9163  divmuldiv  11075  ioojoin  12620  expnlbnd  13313  swrdlend  13748  lcmledvds  15718  pospropd  17520  marrepcl  20775  gsummatr01lem3  20869  upxp  21835  rnelfmlem  22164  brbtwn2  26254  spthonepeq  27104  fh2  29050  homulass  29233  hoadddi  29234  hoadddir  29235  metf1o  34175  rngohomco  34397  rngoisoco  34405  op01dm  35337  paddss12  35973  wessf1ornlem  40294  elaa2  41378  smflimlem2  41907
  Copyright terms: Public domain W3C validator