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

Theorem 3adantl1 1163
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 1147 . 2 ((𝜏𝜑𝜓) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 583 1 (((𝜏𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  3ad2antl2  1183  3ad2antl3  1184  funcnvqp  6406  onfununi  7974  omord2  8189  en2eqpr  9431  divmuldiv  11338  ioojoin  12870  expnlbnd  13599  swrdlend  14015  2cshw  14175  lcmledvds  15941  pospropd  17744  marrepcl  21176  gsummatr01lem3  21269  upxp  22234  rnelfmlem  22563  brbtwn2  26705  wlkonprop  27454  trlsonprop  27503  pthsonprop  27539  spthonprop  27540  spthonepeq  27547  fh2  29408  homulass  29591  hoadddi  29592  hoadddir  29593  metf1o  35141  rngohomco  35360  rngoisoco  35368  op01dm  36427  paddss12  37063  wessf1ornlem  41740  elaa2  42806  smflimlem2  43335
  Copyright terms: Public domain W3C validator