Theorem expcomd 453

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  simplbi2comt  654  ralrimdva  2952  reupick  3870  trintss  4697  pwssun  4944  ordelord  5662  tz7.7  5666  ordtr3OLD  5687  poxp  7176  smores2  7338  smoiun  7345  smogt  7351  tz7.49  7427  omsmolem  7620  mapxpen  8011  f1dmvrnfibi  8133  suplub2  8250  epfrs  8490  r1sdom  8520  rankr1ai  8544  ficardom  8670  cardsdomel  8683  dfac5lem5  8833  cfsmolem  8975  cfcoflem  8977  axdc3lem2  9156  zorn2lem7  9207  genpn0  9704  reclem2pr  9749  supsrlem  9811  ltletr  10008  fzind  11351  rpneg  11739  xrltletr  11864  iccid  12091  ssfzoulel  12428  ssfzo12bi  12429  swrdccatin12lem2  13340  swrdccat  13344  repsdf2  13376  repswswrd  13382  cshwcsh2id  13425  o1rlimmul  14197  dvdsabseq  14873  divalgb  14965  bezoutlem3  15096  ncoprmlnprm  15274  difsqpwdvds  15429  lss1d  18784  pf1ind  19540  chfacfisf  20478  chfacfisfcpmat  20479  cayleyhamilton1  20516  txlm  21261  fmfnfmlem1  21568  blsscls2  22119  metcnpi3  22161  bcmono  24802  nbusgra  25957  redwlk  26136  wwlkextwrd  26256  usg2spot2nb  26592  numclwwlkovf2ex  26613  ocnel  27541  atcvat2i  28630  atcvat4i  28640  dfon2lem5  30936  cgrxfr  31332  colinearxfr  31352  hfelhf  31458  isbasisrelowllem1  32379  isbasisrelowllem2  32380  finxpreclem6  32409  seqpo  32713  atlatle  33625  cvrexchlem  33723  cvrat2  33733  cvrat4  33747  pmapjoin  34156  onfrALTlem2  37782  onfrALTlem2VD  38147  iccpartiltu  39960  iccpartigtl  39961  iccpartlt  39962  lighneal  40066  bgoldbtbnd  40225  tgoldbach  40232  tgoldbachOLD  40239  pfxccatin12lem2  40287  eluzge0nn0  40350  elfz2z  40352  upgrewlkle2  40808  red1wlk  40881  crctcsh1wlkn0lem5  41017  wwlksnextwrd  41103  av-numclwwlkovf2ex  41517  cznnring  41748  ply1mulgsumlem2  41969