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 2696  wereu 2952  f1oun 3713  brecop 4313  genpss 5126  genpnnp 5127  distrlem1pr 5146  ssgt0sr 5236  lemul12itOLD 5852  uzwo5OLD 6220  cau5i 6924  cau5 6926  tgclt 7630  shselt 9280  ficli 10470  homcard 10533  filintf 10562

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