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

Theorem 3adant2r 1318
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
3adant1l.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3adant2r ((𝜑 ∧ (𝜓𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3adant2r
StepHypRef Expression
1 3adant1l.1 . . . 4 ((𝜑𝜓𝜒) → 𝜃)
213com12 1266 . . 3 ((𝜓𝜑𝜒) → 𝜃)
323adant1r 1316 . 2 (((𝜓𝜏) ∧ 𝜑𝜒) → 𝜃)
433com12 1266 1 ((𝜑 ∧ (𝜓𝜏) ∧ 𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  ltdiv23  10858  lediv23  10859  divalglem8  15047  isdrngd  18693  deg1tm  23782  ax5seglem1  25708  ax5seglem2  25709  nvaddsub4  27358  nmoub2i  27475  cdleme21at  35093  cdleme42f  35245  trlcoabs2N  35487  tendoplcl2  35543  tendopltp  35545  cdlemk2  35597  cdlemk8  35603  cdlemk9  35604  cdlemk9bN  35605  cdleml8  35748  dihglblem3N  36061  dihglblem3aN  36062  fourierdlem42  39670  lincscm  41504
  Copyright terms: Public domain W3C validator