Theorem 3adantr2 813

Description: Deduction adding a conjunct to antecedent.

Hypothesis

Ref	Expression
3adantr.1	⊢ ((φ ⋀ (ψ ⋀ χ)) → θ)

Assertion

Ref	Expression
3adantr2	⊢ ((φ ⋀ (ψ ⋀ τ ⋀ χ)) → θ)

Proof of Theorem 3adantr2

Step	Hyp	Ref	Expression
1		3adantr.1	. . . 4 ⊢ ((φ ⋀ (ψ ⋀ χ)) → θ)
2	1	ancoms 438	. . 3 ⊢ (((ψ ⋀ χ) ⋀ φ) → θ)
3	2	3adantl2 810	. 2 ⊢ (((ψ ⋀ τ ⋀ χ) ⋀ φ) → θ)
4	3	ancoms 438	1 ⊢ ((φ ⋀ (ψ ⋀ τ ⋀ χ)) → θ)

Syntax hints:   → wi 3   ⋀ wa 221   ⋀ w3a 781

This theorem is referenced by:  3adant3r2 849  po3nr 2926  bl2in 8053  tgioolem 8125  nvmdi 8517  mdsl3 10524  elicc3 11410  comptoppr 11495  conntoppr 11504  reconnlem1 11507  fipreima 11848  fzm1 11867  sdclem2 11876  sdc 11877  iccss2 11921  icoopnst 11940  iocopnst 11941  totbndss 11993  rrnmet 12072

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145  df-an 223  df-3an 783

Copyright terms: Public domain