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

Theorem 3adantl1 1167
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 1151 . 2 ((𝜏𝜑𝜓) → (𝜑𝜓))
2 3adantl.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylan 581 1 (((𝜏𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  3ad2antl2  1187  3ad2antl3  1188  funcnvqp  6569  onfununi  8291  omord2  8518  en2eqpr  9951  divmuldiv  11863  ioojoin  13409  expnlbnd  14145  swrdlend  14550  2cshw  14710  lcmledvds  16483  pospropd  18224  marrepcl  21936  gsummatr01lem3  22029  upxp  22997  rnelfmlem  23326  brbtwn2  27903  wlkonprop  28655  trlsonprop  28705  pthsonprop  28741  spthonprop  28742  spthonepeq  28749  fh2  30610  homulass  30793  hoadddi  30794  hoadddir  30795  metf1o  36264  rngohomco  36483  rngoisoco  36491  op01dm  37695  paddss12  38332  wessf1ornlem  43495  elaa2  44565  smflimlem2  45103
  Copyright terms: Public domain W3C validator