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  2676  moi  3019  reu6  3025  sbciegft  3076  pwadjoin  4119  nnsucelr  4428  nndisjeq  4429  leltfintr  4458  ssfin  4470  tfinltfinlem1  4500  evenodddisj  4516  spfininduct  4540  vfinspss  4551  iss  5000  funssres  5144  fv3  5341  tz6.12-1  5344  funfvima  5459  funsi  5520  fnpprod  5843  fundmen  6043  enprmaplem6  6081  leltctr  6212  nchoicelem6  6294  nchoicelem17  6305  fnfrec  6320