Theorem im2anan9 563

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 558	1 |- ((ph /\ th) -> ((ps /\ ta) -> (ch /\ et)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  ax11eq 1363  ax11el 1364  trin 2690  wereu 2945  f1oun 3706  brecop 4306  genpss 5107  genpnnp 5108  distrlem1pr 5127  ssgt0sr 5217  lemul12itOLD 5843  uzwo5OLD 6211  cau5i 6917  cau5 6919  tgclt 7624  shselt 9278  ficli 10472  ficliOLD 10473  homcard 10539  filintf 10569

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