Theorem 3adant3l 1322

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

Step	Hyp	Ref	Expression
1		3adant1l.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3com13 1270	. . 3 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)
3	2	3adant1l 1318	. 2 ⊢ (((𝜏 ∧ 𝜒) ∧ 𝜓 ∧ 𝜑) → 𝜃)
4	3	3com13 1270	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 1039

This theorem is referenced by:  wfrlem12  7426  ecopovtrn  7850  rrxmet  23191  nvaddsub4  27512  adjlnop  28945  pl1cn  30001  frrlem11  31792  rrnmet  33628  lflsub  34354  lflmul  34355  cvlatexch3  34625  cdleme5  35527  cdlemeg46rjgN  35810  cdlemg2l  35891  cdlemg10c  35927  tendospcanN  36312  dicvaddcl  36479  dicvscacl  36480  dochexmidlem8  36756  limsupre3lem  39964  fourierdlem42  40366  fourierdlem113  40436  ovnsupge0  40771  ovncvrrp  40778  ovnhoilem2  40816