Theorem expcomd 417

Description: Deduction form of expcom 414. (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 416	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 86	1 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ancomsd  466  simplbi2comt  502  ralrimdva  3140  reupick  4264  pwssun  5517  ordelord  6339  tz7.7  6343  onelssex  6366  poxp  8075  smores2  8291  smoiun  8298  smogt  8304  tz7.49  8381  omsmolem  8590  mapxpen  9078  fodomfir  9235  f1dmvrnfibi  9248  suplub2  9371  epfrs  9650  r1sdom  9696  rankr1ai  9720  ficardom  9883  cardsdomel  9896  dfac5lem5  10047  cfsmolem  10190  cfcoflem  10192  axdc3lem2  10371  zorn2lem7  10422  genpn0  10924  reclem2pr  10969  supsrlem  11032  ltletr  11236  fzind  12625  rpneg  12974  xrltletr  13106  iccid  13341  ssfzoulel  13713  ssfzo12bi  13714  pfxccatin12lem2  14691  swrdccat  14695  repsdf2  14738  repswswrd  14744  cshwcsh2id  14788  o1rlimmul  15579  dvdsabseq  16280  divalgb  16371  bezoutlem3  16508  cncongr1  16634  ncoprmlnprm  16696  difsqpwdvds  16856  lss1d  20960  pf1ind  22348  chfacfisf  22844  chfacfisfcpmat  22845  cayleyhamilton1  22882  txlm  23638  fmfnfmlem1  23944  blsscls2  24494  metcnpi3  24536  bcmono  27265  lestr  27751  elreno2  28512  upgrewlkle2  29700  redwlk  29764  crctcshwlkn0lem5  29907  wwlksnextwrd  29990  clwwlknonex2lem2  30203  ocnel  31394  atcvat2i  32483  atcvat4i  32493  rankfilimb  35290  trssfir1om  35299  trssfir1omregs  35324  dfon2lem5  36020  cgrxfr  36290  colinearxfr  36310  hfelhf  36416  isbasisrelowllem1  37724  isbasisrelowllem2  37725  finxpreclem6  37765  seqpo  38121  atlatle  39819  cvrexchlem  39918  cvrat2  39928  cvrat4  39942  pmapjoin  40351  onfrALTlem2  44997  onfrALTlem2VD  45339  eluzge0nn0  47782  elfz2z  47785  iccpartiltu  47904  iccpartigtl  47905  iccpartlt  47906  lighneal  48096  bgoldbtbnd  48307  tgoldbach  48315  cznnring  48760  ply1mulgsumlem2  48885  itsclc0  49269