Theorem expcomd 420

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  ancomsd  469  simplbi2comt  505  ralrimdva  3110  reupick  4233  pwssun  5451  ordelord  6235  tz7.7  6239  poxp  7895  smores2  8091  smoiun  8098  smogt  8104  tz7.49  8181  omsmolem  8382  mapxpen  8812  f1dmvrnfibi  8960  suplub2  9077  epfrs  9347  r1sdom  9390  rankr1ai  9414  ficardom  9577  cardsdomel  9590  dfac5lem5  9741  cfsmolem  9884  cfcoflem  9886  axdc3lem2  10065  zorn2lem7  10116  genpn0  10617  reclem2pr  10662  supsrlem  10725  ltletr  10924  fzind  12275  rpneg  12618  xrltletr  12747  iccid  12980  ssfzoulel  13336  ssfzo12bi  13337  pfxccatin12lem2  14296  swrdccat  14300  repsdf2  14343  repswswrd  14349  cshwcsh2id  14393  o1rlimmul  15180  dvdsabseq  15874  divalgb  15965  bezoutlem3  16101  cncongr1  16224  ncoprmlnprm  16284  difsqpwdvds  16440  lss1d  20000  pf1ind  21271  chfacfisf  21751  chfacfisfcpmat  21752  cayleyhamilton1  21789  txlm  22545  fmfnfmlem1  22851  blsscls2  23402  metcnpi3  23444  bcmono  26158  upgrewlkle2  27694  redwlk  27760  crctcshwlkn0lem5  27898  wwlksnextwrd  27981  clwwlknonex2lem2  28191  ocnel  29379  atcvat2i  30468  atcvat4i  30478  onelssex  33376  dfon2lem5  33482  sletr  33698  cgrxfr  34094  colinearxfr  34114  hfelhf  34220  isbasisrelowllem1  35263  isbasisrelowllem2  35264  finxpreclem6  35304  seqpo  35642  atlatle  37071  cvrexchlem  37170  cvrat2  37180  cvrat4  37194  pmapjoin  37603  onfrALTlem2  41839  onfrALTlem2VD  42182  eluzge0nn0  44477  elfz2z  44480  iccpartiltu  44547  iccpartigtl  44548  iccpartlt  44549  lighneal  44736  bgoldbtbnd  44934  tgoldbach  44942  cznnring  45187  ply1mulgsumlem2  45401  itsclc0  45790