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  3137  reupick  4269  pwssun  5523  ordelord  6345  tz7.7  6349  onelssex  6372  poxp  8078  smores2  8294  smoiun  8301  smogt  8307  tz7.49  8384  omsmolem  8593  mapxpen  9081  fodomfir  9238  f1dmvrnfibi  9251  suplub2  9374  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  11238  fzind  12627  rpneg  12976  xrltletr  13108  iccid  13343  ssfzoulel  13715  ssfzo12bi  13716  pfxccatin12lem2  14693  swrdccat  14697  repsdf2  14740  repswswrd  14746  cshwcsh2id  14790  o1rlimmul  15581  dvdsabseq  16282  divalgb  16373  bezoutlem3  16510  cncongr1  16636  ncoprmlnprm  16698  difsqpwdvds  16858  lss1d  20958  pf1ind  22320  chfacfisf  22819  chfacfisfcpmat  22820  cayleyhamilton1  22857  txlm  23613  fmfnfmlem1  23919  blsscls2  24469  metcnpi3  24511  bcmono  27240  lestr  27726  elreno2  28487  upgrewlkle2  29675  redwlk  29739  crctcshwlkn0lem5  29882  wwlksnextwrd  29965  clwwlknonex2lem2  30178  ocnel  31369  atcvat2i  32458  atcvat4i  32468  rankfilimb  35245  trssfir1om  35255  trssfir1omregs  35280  dfon2lem5  35967  cgrxfr  36237  colinearxfr  36257  hfelhf  36363  isbasisrelowllem1  37671  isbasisrelowllem2  37672  finxpreclem6  37712  seqpo  38068  atlatle  39766  cvrexchlem  39865  cvrat2  39875  cvrat4  39889  pmapjoin  40298  onfrALTlem2  44973  onfrALTlem2VD  45315  eluzge0nn0  47760  elfz2z  47763  iccpartiltu  47882  iccpartigtl  47883  iccpartlt  47884  lighneal  48074  bgoldbtbnd  48285  tgoldbach  48293  cznnring  48738  ply1mulgsumlem2  48863  itsclc0  49247