Theorem expcomd 417

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

Hypothesis

Ref	Expression
expcomd.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
expcomd	⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

Proof of Theorem expcomd

Step	Hyp	Ref	Expression
1		expcomd.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 416	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 86	1 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  ancomsd  466  simplbi2comt  502  ralrimdva  3106  reupick  4252  pwssun  5485  ordelord  6288  tz7.7  6292  poxp  7969  smores2  8185  smoiun  8192  smogt  8198  tz7.49  8276  omsmolem  8487  mapxpen  8930  f1dmvrnfibi  9103  suplub2  9220  epfrs  9489  r1sdom  9532  rankr1ai  9556  ficardom  9719  cardsdomel  9732  dfac5lem5  9883  cfsmolem  10026  cfcoflem  10028  axdc3lem2  10207  zorn2lem7  10258  genpn0  10759  reclem2pr  10804  supsrlem  10867  ltletr  11067  fzind  12418  rpneg  12762  xrltletr  12891  iccid  13124  ssfzoulel  13481  ssfzo12bi  13482  pfxccatin12lem2  14444  swrdccat  14448  repsdf2  14491  repswswrd  14497  cshwcsh2id  14541  o1rlimmul  15328  dvdsabseq  16022  divalgb  16113  bezoutlem3  16249  cncongr1  16372  ncoprmlnprm  16432  difsqpwdvds  16588  lss1d  20225  pf1ind  21521  chfacfisf  22003  chfacfisfcpmat  22004  cayleyhamilton1  22041  txlm  22799  fmfnfmlem1  23105  blsscls2  23660  metcnpi3  23702  bcmono  26425  upgrewlkle2  27973  redwlk  28040  crctcshwlkn0lem5  28179  wwlksnextwrd  28262  clwwlknonex2lem2  28472  ocnel  29660  atcvat2i  30749  atcvat4i  30759  onelssex  33661  dfon2lem5  33763  sletr  33961  cgrxfr  34357  colinearxfr  34377  hfelhf  34483  isbasisrelowllem1  35526  isbasisrelowllem2  35527  finxpreclem6  35567  seqpo  35905  atlatle  37334  cvrexchlem  37433  cvrat2  37443  cvrat4  37457  pmapjoin  37866  onfrALTlem2  42166  onfrALTlem2VD  42509  eluzge0nn0  44804  elfz2z  44807  iccpartiltu  44874  iccpartigtl  44875  iccpartlt  44876  lighneal  45063  bgoldbtbnd  45261  tgoldbach  45269  cznnring  45514  ply1mulgsumlem2  45728  itsclc0  46117