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  3154  reupick  4329  pwssun  5575  ordelord  6406  tz7.7  6410  onelssex  6432  poxp  8153  smores2  8394  smoiun  8401  smogt  8407  tz7.49  8485  omsmolem  8695  mapxpen  9183  fodomfir  9368  f1dmvrnfibi  9381  suplub2  9501  epfrs  9771  r1sdom  9814  rankr1ai  9838  ficardom  10001  cardsdomel  10014  dfac5lem5  10167  cfsmolem  10310  cfcoflem  10312  axdc3lem2  10491  zorn2lem7  10542  genpn0  11043  reclem2pr  11088  supsrlem  11151  ltletr  11353  fzind  12716  rpneg  13067  xrltletr  13199  iccid  13432  ssfzoulel  13799  ssfzo12bi  13800  pfxccatin12lem2  14769  swrdccat  14773  repsdf2  14816  repswswrd  14822  cshwcsh2id  14867  o1rlimmul  15655  dvdsabseq  16350  divalgb  16441  bezoutlem3  16578  cncongr1  16704  ncoprmlnprm  16765  difsqpwdvds  16925  lss1d  20961  pf1ind  22359  chfacfisf  22860  chfacfisfcpmat  22861  cayleyhamilton1  22898  txlm  23656  fmfnfmlem1  23962  blsscls2  24517  metcnpi3  24559  bcmono  27321  sletr  27803  upgrewlkle2  29624  redwlk  29690  crctcshwlkn0lem5  29834  wwlksnextwrd  29917  clwwlknonex2lem2  30127  ocnel  31317  atcvat2i  32406  atcvat4i  32416  dfon2lem5  35788  cgrxfr  36056  colinearxfr  36076  hfelhf  36182  isbasisrelowllem1  37356  isbasisrelowllem2  37357  finxpreclem6  37397  seqpo  37754  atlatle  39321  cvrexchlem  39421  cvrat2  39431  cvrat4  39445  pmapjoin  39854  onfrALTlem2  44566  onfrALTlem2VD  44909  eluzge0nn0  47324  elfz2z  47327  iccpartiltu  47409  iccpartigtl  47410  iccpartlt  47411  lighneal  47598  bgoldbtbnd  47796  tgoldbach  47804  cznnring  48178  ply1mulgsumlem2  48304  itsclc0  48692