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

This theorem is referenced by:  ancomsd  465  simplbi2comt  501  ralrimdva  3112  reupick  4249  pwssun  5476  ordelord  6273  tz7.7  6277  poxp  7940  smores2  8156  smoiun  8163  smogt  8169  tz7.49  8246  omsmolem  8447  mapxpen  8879  f1dmvrnfibi  9033  suplub2  9150  epfrs  9420  r1sdom  9463  rankr1ai  9487  ficardom  9650  cardsdomel  9663  dfac5lem5  9814  cfsmolem  9957  cfcoflem  9959  axdc3lem2  10138  zorn2lem7  10189  genpn0  10690  reclem2pr  10735  supsrlem  10798  ltletr  10997  fzind  12348  rpneg  12691  xrltletr  12820  iccid  13053  ssfzoulel  13409  ssfzo12bi  13410  pfxccatin12lem2  14372  swrdccat  14376  repsdf2  14419  repswswrd  14425  cshwcsh2id  14469  o1rlimmul  15256  dvdsabseq  15950  divalgb  16041  bezoutlem3  16177  cncongr1  16300  ncoprmlnprm  16360  difsqpwdvds  16516  lss1d  20140  pf1ind  21431  chfacfisf  21911  chfacfisfcpmat  21912  cayleyhamilton1  21949  txlm  22707  fmfnfmlem1  23013  blsscls2  23566  metcnpi3  23608  bcmono  26330  upgrewlkle2  27876  redwlk  27942  crctcshwlkn0lem5  28080  wwlksnextwrd  28163  clwwlknonex2lem2  28373  ocnel  29561  atcvat2i  30650  atcvat4i  30660  onelssex  33563  dfon2lem5  33669  sletr  33888  cgrxfr  34284  colinearxfr  34304  hfelhf  34410  isbasisrelowllem1  35453  isbasisrelowllem2  35454  finxpreclem6  35494  seqpo  35832  atlatle  37261  cvrexchlem  37360  cvrat2  37370  cvrat4  37384  pmapjoin  37793  onfrALTlem2  42055  onfrALTlem2VD  42398  eluzge0nn0  44692  elfz2z  44695  iccpartiltu  44762  iccpartigtl  44763  iccpartlt  44764  lighneal  44951  bgoldbtbnd  45149  tgoldbach  45157  cznnring  45402  ply1mulgsumlem2  45616  itsclc0  46005