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  3134  reupick  4295  pwssun  5533  ordelord  6357  tz7.7  6361  onelssex  6384  poxp  8110  smores2  8326  smoiun  8333  smogt  8339  tz7.49  8416  omsmolem  8624  mapxpen  9113  fodomfir  9286  f1dmvrnfibi  9299  suplub2  9419  epfrs  9691  r1sdom  9734  rankr1ai  9758  ficardom  9921  cardsdomel  9934  dfac5lem5  10087  cfsmolem  10230  cfcoflem  10232  axdc3lem2  10411  zorn2lem7  10462  genpn0  10963  reclem2pr  11008  supsrlem  11071  ltletr  11273  fzind  12639  rpneg  12992  xrltletr  13124  iccid  13358  ssfzoulel  13728  ssfzo12bi  13729  pfxccatin12lem2  14703  swrdccat  14707  repsdf2  14750  repswswrd  14756  cshwcsh2id  14801  o1rlimmul  15592  dvdsabseq  16290  divalgb  16381  bezoutlem3  16518  cncongr1  16644  ncoprmlnprm  16705  difsqpwdvds  16865  lss1d  20876  pf1ind  22249  chfacfisf  22748  chfacfisfcpmat  22749  cayleyhamilton1  22786  txlm  23542  fmfnfmlem1  23848  blsscls2  24399  metcnpi3  24441  bcmono  27195  sletr  27677  upgrewlkle2  29541  redwlk  29607  crctcshwlkn0lem5  29751  wwlksnextwrd  29834  clwwlknonex2lem2  30044  ocnel  31234  atcvat2i  32323  atcvat4i  32333  dfon2lem5  35782  cgrxfr  36050  colinearxfr  36070  hfelhf  36176  isbasisrelowllem1  37350  isbasisrelowllem2  37351  finxpreclem6  37391  seqpo  37748  atlatle  39320  cvrexchlem  39420  cvrat2  39430  cvrat4  39444  pmapjoin  39853  onfrALTlem2  44543  onfrALTlem2VD  44885  eluzge0nn0  47317  elfz2z  47320  iccpartiltu  47427  iccpartigtl  47428  iccpartlt  47429  lighneal  47616  bgoldbtbnd  47814  tgoldbach  47822  cznnring  48254  ply1mulgsumlem2  48380  itsclc0  48764