Theorem expcomd 416

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ancomsd  465  simplbi2comt  501  ralrimdva  3140  reupick  4304  pwssun  5545  ordelord  6374  tz7.7  6378  onelssex  6401  poxp  8127  smores2  8368  smoiun  8375  smogt  8381  tz7.49  8459  omsmolem  8669  mapxpen  9157  fodomfir  9340  f1dmvrnfibi  9353  suplub2  9473  epfrs  9745  r1sdom  9788  rankr1ai  9812  ficardom  9975  cardsdomel  9988  dfac5lem5  10141  cfsmolem  10284  cfcoflem  10286  axdc3lem2  10465  zorn2lem7  10516  genpn0  11017  reclem2pr  11062  supsrlem  11125  ltletr  11327  fzind  12691  rpneg  13041  xrltletr  13173  iccid  13407  ssfzoulel  13776  ssfzo12bi  13777  pfxccatin12lem2  14749  swrdccat  14753  repsdf2  14796  repswswrd  14802  cshwcsh2id  14847  o1rlimmul  15635  dvdsabseq  16332  divalgb  16423  bezoutlem3  16560  cncongr1  16686  ncoprmlnprm  16747  difsqpwdvds  16907  lss1d  20920  pf1ind  22293  chfacfisf  22792  chfacfisfcpmat  22793  cayleyhamilton1  22830  txlm  23586  fmfnfmlem1  23892  blsscls2  24443  metcnpi3  24485  bcmono  27240  sletr  27722  upgrewlkle2  29586  redwlk  29652  crctcshwlkn0lem5  29796  wwlksnextwrd  29879  clwwlknonex2lem2  30089  ocnel  31279  atcvat2i  32368  atcvat4i  32378  dfon2lem5  35805  cgrxfr  36073  colinearxfr  36093  hfelhf  36199  isbasisrelowllem1  37373  isbasisrelowllem2  37374  finxpreclem6  37414  seqpo  37771  atlatle  39338  cvrexchlem  39438  cvrat2  39448  cvrat4  39462  pmapjoin  39871  onfrALTlem2  44571  onfrALTlem2VD  44913  eluzge0nn0  47341  elfz2z  47344  iccpartiltu  47436  iccpartigtl  47437  iccpartlt  47438  lighneal  47625  bgoldbtbnd  47823  tgoldbach  47831  cznnring  48237  ply1mulgsumlem2  48363  itsclc0  48751