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

Theorem 3adantl1 1237
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 1080 . 2 ((𝜏𝜑𝜓) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 487 1 (((𝜏𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  3ad2antl2  1244  3ad2antl3  1245  funcnvqp  5990  onfununi  7483  omord2  7692  en2eqpr  8868  divmuldiv  10763  ioojoin  12341  expnlbnd  13034  swrdlend  13477  lcmledvds  15359  pospropd  17181  marrepcl  20418  gsummatr01lem3  20511  upxp  21474  rnelfmlem  21803  brbtwn2  25830  spthonepeq  26704  fh2  28606  homulass  28789  hoadddi  28790  hoadddir  28791  metf1o  33681  rngohomco  33903  rngoisoco  33911  op01dm  34788  paddss12  35423  wessf1ornlem  39685  elaa2  40769  smflimlem2  41301
  Copyright terms: Public domain W3C validator