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  3144  reupick  4319  pwssun  5568  ordelord  6388  tz7.7  6392  onelssex  6414  poxp  8132  smores2  8374  smoiun  8381  smogt  8387  tz7.49  8465  omsmolem  8677  mapxpen  9171  fodomfir  9361  f1dmvrnfibi  9374  suplub2  9495  epfrs  9765  r1sdom  9808  rankr1ai  9832  ficardom  9995  cardsdomel  10008  dfac5lem5  10161  cfsmolem  10302  cfcoflem  10304  axdc3lem2  10483  zorn2lem7  10534  genpn0  11035  reclem2pr  11080  supsrlem  11143  ltletr  11345  fzind  12704  rpneg  13052  xrltletr  13182  iccid  13415  ssfzoulel  13772  ssfzo12bi  13773  pfxccatin12lem2  14732  swrdccat  14736  repsdf2  14779  repswswrd  14785  cshwcsh2id  14830  o1rlimmul  15614  dvdsabseq  16308  divalgb  16399  bezoutlem3  16535  cncongr1  16661  ncoprmlnprm  16723  difsqpwdvds  16882  lss1d  20934  pf1ind  22341  chfacfisf  22842  chfacfisfcpmat  22843  cayleyhamilton1  22880  txlm  23638  fmfnfmlem1  23944  blsscls2  24499  metcnpi3  24541  bcmono  27301  sletr  27783  upgrewlkle2  29538  redwlk  29604  crctcshwlkn0lem5  29743  wwlksnextwrd  29826  clwwlknonex2lem2  30036  ocnel  31226  atcvat2i  32315  atcvat4i  32325  dfon2lem5  35622  cgrxfr  35890  colinearxfr  35910  hfelhf  36016  isbasisrelowllem1  37073  isbasisrelowllem2  37074  finxpreclem6  37114  seqpo  37459  atlatle  39029  cvrexchlem  39129  cvrat2  39139  cvrat4  39153  pmapjoin  39562  onfrALTlem2  44257  onfrALTlem2VD  44600  eluzge0nn0  46959  elfz2z  46962  iccpartiltu  47028  iccpartigtl  47029  iccpartlt  47030  lighneal  47217  bgoldbtbnd  47415  tgoldbach  47423  cznnring  47673  ply1mulgsumlem2  47804  itsclc0  48193