Theorem 3adant3l 1314

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 1262	. . 3 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)
3	2	3adant1l 1310	. 2 ⊢ (((𝜏 ∧ 𝜒) ∧ 𝜓 ∧ 𝜑) → 𝜃)
4	3	3com13 1262	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  wfrlem12  7313  ecopovtrn  7737  rrxmet  22999  nvaddsub4  26896  adjlnop  28329  pl1cn  29329  frrlem11  31036  rrnmet  32798  lflsub  33372  lflmul  33373  cvlatexch3  33643  cdleme5  34545  cdlemeg46rjgN  34828  cdlemg2l  34909  cdlemg10c  34945  tendospcanN  35330  dicvaddcl  35497  dicvscacl  35498  dochexmidlem8  35774  fourierdlem42  39042  fourierdlem113  39112  ovnsupge0  39447  ovncvrrp  39454  ovnhoilem2  39492