Theorem im2anan9 565

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 391	. 2 |- ((ph /\ th) -> (ps -> ch))
3		im2an9.2	. . 3 |- (th -> (ta -> et))
4	3	adantl 390	. 2 |- ((ph /\ th) -> (ta -> et))
5	2, 4	anim12d 560	1 |- ((ph /\ th) -> ((ps /\ ta) -> (ch /\ et)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  ax11eq 1365  ax11el 1366  trin 2695  wereu 2951  f1oun 3712  brecop 4312  genpss 5119  genpnnp 5120  distrlem1pr 5139  ssgt0sr 5229  lemul12itOLD 5845  uzwo5OLD 6213  cau5i 6917  cau5 6919  tgclt 7623  shselt 9273  ficli 10462  homcard 10525  filintf 10554

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