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  3138  reupick  4283  pwssun  5524  ordelord  6347  tz7.7  6351  onelssex  6374  poxp  8080  smores2  8296  smoiun  8303  smogt  8309  tz7.49  8386  omsmolem  8595  mapxpen  9083  fodomfir  9240  f1dmvrnfibi  9253  suplub2  9376  epfrs  9652  r1sdom  9698  rankr1ai  9722  ficardom  9885  cardsdomel  9898  dfac5lem5  10049  cfsmolem  10192  cfcoflem  10194  axdc3lem2  10373  zorn2lem7  10424  genpn0  10926  reclem2pr  10971  supsrlem  11034  ltletr  11237  fzind  12602  rpneg  12951  xrltletr  13083  iccid  13318  ssfzoulel  13688  ssfzo12bi  13689  pfxccatin12lem2  14666  swrdccat  14670  repsdf2  14713  repswswrd  14719  cshwcsh2id  14763  o1rlimmul  15554  dvdsabseq  16252  divalgb  16343  bezoutlem3  16480  cncongr1  16606  ncoprmlnprm  16667  difsqpwdvds  16827  lss1d  20926  pf1ind  22311  chfacfisf  22810  chfacfisfcpmat  22811  cayleyhamilton1  22848  txlm  23604  fmfnfmlem1  23910  blsscls2  24460  metcnpi3  24502  bcmono  27256  lestr  27742  elreno2  28503  upgrewlkle2  29692  redwlk  29756  crctcshwlkn0lem5  29899  wwlksnextwrd  29982  clwwlknonex2lem2  30195  ocnel  31385  atcvat2i  32474  atcvat4i  32484  rankfilimb  35277  trssfir1om  35286  trssfir1omregs  35311  dfon2lem5  35998  cgrxfr  36268  colinearxfr  36288  hfelhf  36394  isbasisrelowllem1  37604  isbasisrelowllem2  37605  finxpreclem6  37645  seqpo  37992  atlatle  39690  cvrexchlem  39789  cvrat2  39799  cvrat4  39813  pmapjoin  40222  onfrALTlem2  44896  onfrALTlem2VD  45238  eluzge0nn0  47666  elfz2z  47669  iccpartiltu  47776  iccpartigtl  47777  iccpartlt  47778  lighneal  47965  bgoldbtbnd  48163  tgoldbach  48171  cznnring  48616  ply1mulgsumlem2  48741  itsclc0  49125