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

Theorem 3adantl1 1171
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 1146 . 2 ((𝜏𝜑𝜓) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 569 1 (((𝜏𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  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 197  df-an 383  df-3an 1073
This theorem is referenced by:  3ad2antl2  1201  3ad2antl3  1202  funcnvqp  6093  onfununi  7591  omord2  7801  en2eqpr  9030  divmuldiv  10927  ioojoin  12510  expnlbnd  13201  swrdlend  13640  lcmledvds  15520  pospropd  17342  marrepcl  20588  gsummatr01lem3  20682  upxp  21647  rnelfmlem  21976  brbtwn2  26006  spthonepeq  26883  fh2  28818  homulass  29001  hoadddi  29002  hoadddir  29003  metf1o  33883  rngohomco  34105  rngoisoco  34113  op01dm  34992  paddss12  35627  wessf1ornlem  39891  elaa2  40968  smflimlem2  41500
  Copyright terms: Public domain W3C validator