Theorem expcomd 436

Description: Deduction form of expcom 433. (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 434	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 78	1 |- ( ph -> ( ch -> ( ps -> th ) ) )

Syntax hints:   -> wi 4   /\ wa 367

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 185  df-an 369

This theorem is referenced by:  simplbi2comt  624  ralrimdva  2872  reupick  3779  trintss  4548  pwssun  4775  ordelord  4889  tz7.7  4893  poxp  6885  smores2  7017  smoiun  7024  smogt  7030  tz7.49  7102  omsmolem  7294  mapxpen  7676  suplub2  7912  epfrs  8153  r1sdom  8183  rankr1ai  8207  ficardom  8333  cardsdomel  8346  dfac5lem5  8499  cfsmolem  8641  cfcoflem  8643  axdc3lem2  8822  zorn2lem7  8873  genpn0  9370  reclem2pr  9415  supsrlem  9477  ltletr  9665  fzind  10958  rpneg  11251  xrltletr  11363  iccid  11577  ssfzoulel  11887  ssfzo12bi  11888  swrdccatin12lem2  12705  swrdccat  12709  repsdf2  12741  repswswrd  12747  cshwcsh2id  12787  o1rlimmul  13523  divalgb  14146  bezoutlem3  14262  lss1d  17804  pf1ind  18586  chfacfisf  19522  chfacfisfcpmat  19523  cayleyhamilton1  19560  txlm  20315  fmfnfmlem1  20621  blsscls2  21173  metcnpi3  21215  bcmono  23750  nbusgra  24630  redwlk  24810  wwlkextwrd  24930  usg2spot2nb  25267  numclwwlkovf2ex  25288  ocnel  26414  atcvat2i  27504  atcvat4i  27514  dfon2lem5  29459  cgrxfr  29933  colinearxfr  29953  hfelhf  30066  seqpo  30480  pfxccatin12lem2  32652  f1dmvrnfibi  32686  eluzge0nn0  32703  elfz2z  32705  cznnring  33018  ply1mulgsumlem2  33241  onfrALTlem2  33712  onfrALTlem2VD  34090  atlatle  35442  cvrexchlem  35540  cvrat2  35550  cvrat4  35564  pmapjoin  35973