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  3151  reupick  4334  pwssun  5579  ordelord  6407  tz7.7  6411  onelssex  6433  poxp  8151  smores2  8392  smoiun  8399  smogt  8405  tz7.49  8483  omsmolem  8693  mapxpen  9181  fodomfir  9365  f1dmvrnfibi  9378  suplub2  9498  epfrs  9768  r1sdom  9811  rankr1ai  9835  ficardom  9998  cardsdomel  10011  dfac5lem5  10164  cfsmolem  10307  cfcoflem  10309  axdc3lem2  10488  zorn2lem7  10539  genpn0  11040  reclem2pr  11085  supsrlem  11148  ltletr  11350  fzind  12713  rpneg  13064  xrltletr  13195  iccid  13428  ssfzoulel  13795  ssfzo12bi  13796  pfxccatin12lem2  14765  swrdccat  14769  repsdf2  14812  repswswrd  14818  cshwcsh2id  14863  o1rlimmul  15651  dvdsabseq  16346  divalgb  16437  bezoutlem3  16574  cncongr1  16700  ncoprmlnprm  16761  difsqpwdvds  16920  lss1d  20978  pf1ind  22374  chfacfisf  22875  chfacfisfcpmat  22876  cayleyhamilton1  22913  txlm  23671  fmfnfmlem1  23977  blsscls2  24532  metcnpi3  24574  bcmono  27335  sletr  27817  upgrewlkle2  29638  redwlk  29704  crctcshwlkn0lem5  29843  wwlksnextwrd  29926  clwwlknonex2lem2  30136  ocnel  31326  atcvat2i  32415  atcvat4i  32425  dfon2lem5  35768  cgrxfr  36036  colinearxfr  36056  hfelhf  36162  isbasisrelowllem1  37337  isbasisrelowllem2  37338  finxpreclem6  37378  seqpo  37733  atlatle  39301  cvrexchlem  39401  cvrat2  39411  cvrat4  39425  pmapjoin  39834  onfrALTlem2  44543  onfrALTlem2VD  44886  eluzge0nn0  47261  elfz2z  47264  iccpartiltu  47346  iccpartigtl  47347  iccpartlt  47348  lighneal  47535  bgoldbtbnd  47733  tgoldbach  47741  cznnring  48105  ply1mulgsumlem2  48232  itsclc0  48620