Theorem expcomd 444

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

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  simplbi2comt  636  ralrimdva  2793  reupick  3695  trintss  4485  pwssun  4718  ordelord  5424  tz7.7  5428  poxp  6896  smores2  7060  smoiun  7067  smogt  7073  tz7.49  7149  omsmolem  7341  mapxpen  7725  f1dmvrnfibi  7845  suplub2  7962  epfrs  8202  r1sdom  8232  rankr1ai  8256  ficardom  8382  cardsdomel  8395  dfac5lem5  8545  cfsmolem  8687  cfcoflem  8689  axdc3lem2  8868  zorn2lem7  8919  genpn0  9415  reclem2pr  9460  supsrlem  9522  ltletr  9712  fzind  11023  rpneg  11322  xrltletr  11444  iccid  11671  ssfzoulel  11998  ssfzo12bi  11999  swrdccatin12lem2  12844  swrdccat  12848  repsdf2  12880  repswswrd  12886  cshwcsh2id  12926  o1rlimmul  13693  divalgb  14396  bezoutlem3OLD  14516  bezoutlem3  14519  ncoprmlnprm  14688  lss1d  18197  pf1ind  18954  chfacfisf  19889  chfacfisfcpmat  19890  cayleyhamilton1  19927  txlm  20674  fmfnfmlem1  20980  blsscls2  21530  metcnpi3  21572  bcmono  24217  nbusgra  25168  redwlk  25348  wwlkextwrd  25468  usg2spot2nb  25805  numclwwlkovf2ex  25826  ocnel  26963  atcvat2i  28052  atcvat4i  28062  dfon2lem5  30439  cgrxfr  30828  colinearxfr  30848  hfelhf  30954  isbasisrelowllem1  31760  isbasisrelowllem2  31761  finxpreclem6  31790  seqpo  32078  atlatle  32888  cvrexchlem  32986  cvrat2  32996  cvrat4  33010  pmapjoin  33419  onfrALTlem2  36913  onfrALTlem2VD  37283  iccpartiltu  38827  iccpartigtl  38828  iccpartlt  38829  bgoldbtbnd  38995  tgoldbach  39002  pfxccatin12lem2  39058  eluzge0nn0  39147  elfz2z  39149  upgrewlkle2  39725  red1wlk  39769  cznnring  40283  ply1mulgsumlem2  40504