Theorem expcomd 438

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

Syntax hints:   -> wi 4   /\ wa 369

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 371

This theorem is referenced by:  simplbi2comt  626  reupick  3734  trintss  4501  pwssun  4727  ordelord  4841  tz7.7  4845  poxp  6786  smores2  6917  smoiun  6924  smogt  6930  tz7.49  7002  omsmolem  7194  mapxpen  7579  suplub2  7814  epfrs  8054  r1sdom  8084  rankr1ai  8108  ficardom  8234  cardsdomel  8247  dfac5lem5  8400  cfsmolem  8542  cfcoflem  8544  axdc3lem2  8723  zorn2lem7  8774  genpn0  9275  reclem2pr  9320  supsrlem  9381  ltletr  9569  uzletr  10972  rpneg  11123  xrltletr  11234  iccid  11448  ssfzoulel  11724  swrdccatin12lem2  12484  repsdf2  12520  repswswrd  12526  o1rlimmul  13200  divalgb  13712  bezoutlem3  13828  lss1d  17152  pf1ind  17900  txlm  19339  fmfnfmlem1  19645  blsscls2  20197  metcnpi3  20239  bcmono  22734  nbusgra  23476  redwlk  23642  ocnel  24838  atcvat2i  25928  atcvat4i  25938  dfon2lem5  27736  cgrxfr  28222  colinearxfr  28242  hfelhf  28355  seqpo  28783  eluzge0nn0  30329  uzuzle  30330  elfz2z  30338  wwlkextwrd  30500  erclwwlktr0  30619  usg2spot2nb  30798  numclwwlkovf2ex  30819  ply1mulgsumlem2  30989  chfacfisf  31310  chfacfisfcpmat  31311  cayleyhamilton1  31349  onfrALTlem2  31556  onfrALTlem2VD  31927  atlatle  33273  cvrexchlem  33371  cvrat2  33381  cvrat4  33395  pmapjoin  33804