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

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

Proof of Theorem 3adant3l
StepHypRef Expression
1 3adant1l.1 . . . 4 ((𝜑𝜓𝜒) → 𝜃)
213com13 1268 . . 3 ((𝜒𝜓𝜑) → 𝜃)
323adant1l 1316 . 2 (((𝜏𝜒) ∧ 𝜓𝜑) → 𝜃)
433com13 1268 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:  wfrlem12  7411  ecopovtrn  7835  rrxmet  23172  nvaddsub4  27482  adjlnop  28915  pl1cn  29975  frrlem11  31766  rrnmet  33599  lflsub  34173  lflmul  34174  cvlatexch3  34444  cdleme5  35346  cdlemeg46rjgN  35629  cdlemg2l  35710  cdlemg10c  35746  tendospcanN  36131  dicvaddcl  36298  dicvscacl  36299  dochexmidlem8  36575  limsupre3lem  39764  fourierdlem42  40129  fourierdlem113  40199  ovnsupge0  40534  ovncvrrp  40541  ovnhoilem2  40579
 Copyright terms: Public domain W3C validator