Theorem expcomd 454

Description: Deduction form of expcom 451. (Contributed by Alan Sare, 22-Jul-2012.)

Hypothesis

Ref	Expression
expcomd.1	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Assertion

Ref	Expression
expcomd	|- ( ph -> ( ch -> ( ps -> th ) ) )

Proof of Theorem expcomd

Step	Hyp	Ref	Expression
1		expcomd.1	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
2	1	expd 452	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 86	1 |- ( ph -> ( ch -> ( ps -> th ) ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  simplbi2comt  656  ralrimdva  2969  reupick  3911  trintssOLD  4770  pwssun  5020  ordelord  5745  tz7.7  5749  ordtr3OLD  5770  poxp  7289  smores2  7451  smoiun  7458  smogt  7464  tz7.49  7540  omsmolem  7733  mapxpen  8126  f1dmvrnfibi  8250  suplub2  8367  epfrs  8607  r1sdom  8637  rankr1ai  8661  ficardom  8787  cardsdomel  8800  dfac5lem5  8950  cfsmolem  9092  cfcoflem  9094  axdc3lem2  9273  zorn2lem7  9324  genpn0  9825  reclem2pr  9870  supsrlem  9932  ltletr  10129  fzind  11475  rpneg  11863  xrltletr  11988  iccid  12220  ssfzoulel  12562  ssfzo12bi  12563  swrdccatin12lem2  13489  swrdccat  13493  repsdf2  13525  repswswrd  13531  cshwcsh2id  13574  o1rlimmul  14349  dvdsabseq  15035  divalgb  15127  bezoutlem3  15258  cncongr1  15381  ncoprmlnprm  15436  difsqpwdvds  15591  lss1d  18963  pf1ind  19719  chfacfisf  20659  chfacfisfcpmat  20660  cayleyhamilton1  20697  txlm  21451  fmfnfmlem1  21758  blsscls2  22309  metcnpi3  22351  bcmono  25002  upgrewlkle2  26502  redwlk  26569  crctcshwlkn0lem5  26706  wwlksnextwrd  26792  numclwwlkovf2exlem2  27212  ocnel  28157  atcvat2i  29246  atcvat4i  29256  dfon2lem5  31692  sletr  31883  cgrxfr  32162  colinearxfr  32182  hfelhf  32288  isbasisrelowllem1  33203  isbasisrelowllem2  33204  finxpreclem6  33233  seqpo  33543  atlatle  34607  cvrexchlem  34705  cvrat2  34715  cvrat4  34729  pmapjoin  35138  onfrALTlem2  38761  onfrALTlem2VD  39125  eluzge0nn0  41322  elfz2z  41325  iccpartiltu  41358  iccpartigtl  41359  iccpartlt  41360  pfxccatin12lem2  41424  lighneal  41528  bgoldbtbnd  41697  tgoldbach  41705  tgoldbachOLD  41712  cznnring  41956  ply1mulgsumlem2  42175