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

This theorem is referenced by:  ancomsd  466  simplbi2comt  502  ralrimdva  3147  reupick  4264  pwssun  5509  ordelord  6318  tz7.7  6322  poxp  8028  smores2  8247  smoiun  8254  smogt  8260  tz7.49  8338  omsmolem  8550  mapxpen  9000  f1dmvrnfibi  9193  suplub2  9310  epfrs  9580  r1sdom  9623  rankr1ai  9647  ficardom  9810  cardsdomel  9823  dfac5lem5  9976  cfsmolem  10119  cfcoflem  10121  axdc3lem2  10300  zorn2lem7  10351  genpn0  10852  reclem2pr  10897  supsrlem  10960  ltletr  11160  fzind  12511  rpneg  12855  xrltletr  12984  iccid  13217  ssfzoulel  13574  ssfzo12bi  13575  pfxccatin12lem2  14534  swrdccat  14538  repsdf2  14581  repswswrd  14587  cshwcsh2id  14632  o1rlimmul  15419  dvdsabseq  16113  divalgb  16204  bezoutlem3  16340  cncongr1  16461  ncoprmlnprm  16521  difsqpwdvds  16677  lss1d  20323  pf1ind  21619  chfacfisf  22101  chfacfisfcpmat  22102  cayleyhamilton1  22139  txlm  22897  fmfnfmlem1  23203  blsscls2  23758  metcnpi3  23800  bcmono  26523  upgrewlkle2  28175  redwlk  28241  crctcshwlkn0lem5  28380  wwlksnextwrd  28463  clwwlknonex2lem2  28673  ocnel  29861  atcvat2i  30950  atcvat4i  30960  onelssex  33871  dfon2lem5  33962  sletr  34052  cgrxfr  34448  colinearxfr  34468  hfelhf  34574  isbasisrelowllem1  35624  isbasisrelowllem2  35625  finxpreclem6  35665  seqpo  36003  atlatle  37580  cvrexchlem  37680  cvrat2  37690  cvrat4  37704  pmapjoin  38113  onfrALTlem2  42476  onfrALTlem2VD  42819  eluzge0nn0  45144  elfz2z  45147  iccpartiltu  45214  iccpartigtl  45215  iccpartlt  45216  lighneal  45403  bgoldbtbnd  45601  tgoldbach  45609  cznnring  45854  ply1mulgsumlem2  46068  itsclc0  46457