Theorem im2anan9 622

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  ax11eq 1754  ax11el 1755  trin 3422  wereu 3654  xpss12 4089  f1oun 4658  brecop 5365  genpss 6259  genpnnp 6260  distrlem1pr 6279  ssgt0sr 6369  lemul12aOLD 7025  uzwo5OLD 7423  cau5ii 8169  cau5i 8171  tgcl 8894  ringideu 9470  filintf 10274  shsel 10911  soxp 13950  axfelem14 14044  ficli 14353  cbicplem 14508  ridlideq 14695  homcard 14893  lvsovso 15038  tarcrpr 15237  ringideuNEW 17146

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 164  df-an 242

Copyright terms: Public domain