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

Theorem 3adantl1 1164
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 1148 . 2 ((𝜏𝜑𝜓) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 579 1 (((𝜏𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1085
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 396  df-3an 1087
This theorem is referenced by:  3ad2antl2  1184  3ad2antl3  1185  funcnvqp  6482  onfununi  8143  omord2  8360  en2eqpr  9694  divmuldiv  11605  ioojoin  13144  expnlbnd  13876  swrdlend  14294  2cshw  14454  lcmledvds  16232  pospropd  17960  marrepcl  21621  gsummatr01lem3  21714  upxp  22682  rnelfmlem  23011  brbtwn2  27176  wlkonprop  27928  trlsonprop  27977  pthsonprop  28013  spthonprop  28014  spthonepeq  28021  fh2  29882  homulass  30065  hoadddi  30066  hoadddir  30067  metf1o  35840  rngohomco  36059  rngoisoco  36067  op01dm  37124  paddss12  37760  wessf1ornlem  42611  elaa2  43665  smflimlem2  44194
  Copyright terms: Public domain W3C validator