Theorem expcomd 415

Description: Deduction form of expcom 412. (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 414	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 86	1 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  ancomsd  464  simplbi2comt  500  ralrimdva  3152  reupick  4317  pwssun  5570  ordelord  6385  tz7.7  6389  onelssex  6411  poxp  8116  smores2  8356  smoiun  8363  smogt  8369  tz7.49  8447  omsmolem  8658  mapxpen  9145  f1dmvrnfibi  9338  suplub2  9458  epfrs  9728  r1sdom  9771  rankr1ai  9795  ficardom  9958  cardsdomel  9971  dfac5lem5  10124  cfsmolem  10267  cfcoflem  10269  axdc3lem2  10448  zorn2lem7  10499  genpn0  11000  reclem2pr  11045  supsrlem  11108  ltletr  11310  fzind  12664  rpneg  13010  xrltletr  13140  iccid  13373  ssfzoulel  13730  ssfzo12bi  13731  pfxccatin12lem2  14685  swrdccat  14689  repsdf2  14732  repswswrd  14738  cshwcsh2id  14783  o1rlimmul  15567  dvdsabseq  16260  divalgb  16351  bezoutlem3  16487  cncongr1  16608  ncoprmlnprm  16668  difsqpwdvds  16824  lss1d  20718  pf1ind  22094  chfacfisf  22576  chfacfisfcpmat  22577  cayleyhamilton1  22614  txlm  23372  fmfnfmlem1  23678  blsscls2  24233  metcnpi3  24275  bcmono  27016  sletr  27497  upgrewlkle2  29130  redwlk  29196  crctcshwlkn0lem5  29335  wwlksnextwrd  29418  clwwlknonex2lem2  29628  ocnel  30818  atcvat2i  31907  atcvat4i  31917  dfon2lem5  35063  cgrxfr  35331  colinearxfr  35351  hfelhf  35457  isbasisrelowllem1  36539  isbasisrelowllem2  36540  finxpreclem6  36580  seqpo  36918  atlatle  38493  cvrexchlem  38593  cvrat2  38603  cvrat4  38617  pmapjoin  39026  onfrALTlem2  43609  onfrALTlem2VD  43952  eluzge0nn0  46318  elfz2z  46321  iccpartiltu  46388  iccpartigtl  46389  iccpartlt  46390  lighneal  46577  bgoldbtbnd  46775  tgoldbach  46783  cznnring  46942  ply1mulgsumlem2  47155  itsclc0  47544