Theorem adantrrr 405

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem adantrrr

Step	Hyp	Ref	Expression
1		adantr2.1	. . . 4 ⊢ ((φ ⋀ (ψ ⋀ χ)) → θ)
2	1	a1d 12	. . 3 ⊢ ((φ ⋀ (ψ ⋀ χ)) → (τ → θ))
3	2	exp32 379	. 2 ⊢ (φ → (ψ → (χ → (τ → θ))))
4	3	imp45 372	1 ⊢ ((φ ⋀ (ψ ⋀ (χ ⋀ τ))) → θ)

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  supmo 4591  zorn2lem6 4810  lemul12b 5854  lediv12a 5910  climsqueezei 7172  climsqueeze2i 7173  caucvglem6 7194  cvgratlem1 7282  tgcl 7654  tgss2 7667  neissex 7764  opni3 7892  iscau3 7964  iscau4 7966  bopcnlem2 8008  bcthlem17 8041  abl4 8130  ubthlem12 8565  shscli 9305  nlelchi 10018  mdslmd3i 10284

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 147  df-an 225

Copyright terms: Public domain