Theorem imp3a 420

Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)

Hypothesis

Ref	Expression
imp3.1	|- (ph -> (ps -> (ch -> th)))

Assertion

Ref	Expression
imp3a	|- (ph -> ((ps /\ ch) -> th))

Proof of Theorem imp3a

Step	Hyp	Ref	Expression
1		imp3.1	. . . 4 |- (ph -> (ps -> (ch -> th)))
2	1	com3l 75	. . 3 |- (ps -> (ch -> (ph -> th)))
3	2	imp 418	. 2 |- ((ps /\ ch) -> (ph -> th))
4	3	com12 27	1 |- (ph -> ((ps /\ ch) -> th))

Syntax hints:   -> wi 4   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  imp32  422  pm3.31  432  syland  467  imp4c  574  imp4d  575  imp5d  582  expimpd  586  expl  601  3expib  1154  equs5  1996  sbied  2036  rsp2  2677  moi  3020  reu6  3026  sbciegft  3077  pwadjoin  4120  nnsucelr  4429  nndisjeq  4430  leltfintr  4459  ssfin  4471  tfinltfinlem1  4501  evenodddisj  4517  spfininduct  4541  vfinspss  4552  iss  5001  funssres  5145  fv3  5342  tz6.12-1  5345  funfvima  5460  funsi  5521  fnpprod  5844  fundmen  6044  enprmaplem6  6082  leltctr  6213  nchoicelem6  6295  nchoicelem17  6306  fnfrec  6321