Theorem im2anan9 562

Description: Deduction joining nested implications to form implication of conjunctions.

Hypotheses

Ref	Expression
im2an9.1	|- (ph -> (ps -> ch))
im2an9.2	|- (th -> (ta -> et))

Assertion

Ref	Expression
im2anan9	|- ((ph /\ th) -> ((ps /\ ta) -> (ch /\ et)))

Proof of Theorem im2anan9

Step	Hyp	Ref	Expression
1		im2an9.1	. . 3 |- (ph -> (ps -> ch))
2	1	adantr 389	. 2 |- ((ph /\ th) -> (ps -> ch))
3		im2an9.2	. . 3 |- (th -> (ta -> et))
4	3	adantl 388	. 2 |- ((ph /\ th) -> (ta -> et))
5	2, 4	anim12d 557	1 |- ((ph /\ th) -> ((ps /\ ta) -> (ch /\ et)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  ax11eq 1361  ax11el 1362  trin 2685  wereu 2940  f1oun 3697  brecop 4296  genpss 5087  genpnnp 5088  distrlem1pr 5107  ssgt0sr 5197  lemul12itOLD 5807  uzwo5OLD 6167  cau5i 6862  cau5 6864  tgclt 7574  shselt 9216  ficli 10404  homcard 10462  filintf 10479

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