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

Theorem 3adantl1 1209
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 1052 . 2 ((𝜏𝜑𝜓) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 486 1 (((𝜏𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  3ad2antl2  1216  3ad2antl3  1217  funcnvqp  5852  onfununi  7303  omord2  7512  en2eqpr  8691  divmuldiv  10577  ioojoin  12133  expnlbnd  12814  swrdlend  13232  lcmledvds  15099  pospropd  16906  marrepcl  20137  gsummatr01lem3  20230  upxp  21184  rnelfmlem  21514  brbtwn2  25531  fh2  27696  homulass  27879  hoadddi  27880  hoadddir  27881  metf1o  32545  rngohomco  32767  rngoisoco  32775  op01dm  33312  paddss12  33947  wessf1ornlem  38190  elaa2  38951  smflimlem2  39482  spthonepeq-av  40980
  Copyright terms: Public domain W3C validator