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  3136  reupick  4281  pwssun  5516  ordelord  6339  tz7.7  6343  onelssex  6366  poxp  8070  smores2  8286  smoiun  8293  smogt  8299  tz7.49  8376  omsmolem  8585  mapxpen  9071  fodomfir  9228  f1dmvrnfibi  9241  suplub2  9364  epfrs  9640  r1sdom  9686  rankr1ai  9710  ficardom  9873  cardsdomel  9886  dfac5lem5  10037  cfsmolem  10180  cfcoflem  10182  axdc3lem2  10361  zorn2lem7  10412  genpn0  10914  reclem2pr  10959  supsrlem  11022  ltletr  11225  fzind  12590  rpneg  12939  xrltletr  13071  iccid  13306  ssfzoulel  13676  ssfzo12bi  13677  pfxccatin12lem2  14654  swrdccat  14658  repsdf2  14701  repswswrd  14707  cshwcsh2id  14751  o1rlimmul  15542  dvdsabseq  16240  divalgb  16331  bezoutlem3  16468  cncongr1  16594  ncoprmlnprm  16655  difsqpwdvds  16815  lss1d  20914  pf1ind  22299  chfacfisf  22798  chfacfisfcpmat  22799  cayleyhamilton1  22836  txlm  23592  fmfnfmlem1  23898  blsscls2  24448  metcnpi3  24490  bcmono  27244  lestr  27730  elreno2  28491  upgrewlkle2  29680  redwlk  29744  crctcshwlkn0lem5  29887  wwlksnextwrd  29970  clwwlknonex2lem2  30183  ocnel  31373  atcvat2i  32462  atcvat4i  32472  rankfilimb  35258  trssfir1om  35267  trssfir1omregs  35292  dfon2lem5  35979  cgrxfr  36249  colinearxfr  36269  hfelhf  36375  isbasisrelowllem1  37556  isbasisrelowllem2  37557  finxpreclem6  37597  seqpo  37944  atlatle  39576  cvrexchlem  39675  cvrat2  39685  cvrat4  39699  pmapjoin  40108  onfrALTlem2  44783  onfrALTlem2VD  45125  eluzge0nn0  47554  elfz2z  47557  iccpartiltu  47664  iccpartigtl  47665  iccpartlt  47666  lighneal  47853  bgoldbtbnd  48051  tgoldbach  48059  cznnring  48504  ply1mulgsumlem2  48629  itsclc0  49013