Theorem expcomd 418

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  ancomsd  467  simplbi2comt  503  ralrimdva  3155  reupick  4319  pwssun  5572  ordelord  6387  tz7.7  6391  onelssex  6413  poxp  8114  smores2  8354  smoiun  8361  smogt  8367  tz7.49  8445  omsmolem  8656  mapxpen  9143  f1dmvrnfibi  9336  suplub2  9456  epfrs  9726  r1sdom  9769  rankr1ai  9793  ficardom  9956  cardsdomel  9969  dfac5lem5  10122  cfsmolem  10265  cfcoflem  10267  axdc3lem2  10446  zorn2lem7  10497  genpn0  10998  reclem2pr  11043  supsrlem  11106  ltletr  11306  fzind  12660  rpneg  13006  xrltletr  13136  iccid  13369  ssfzoulel  13726  ssfzo12bi  13727  pfxccatin12lem2  14681  swrdccat  14685  repsdf2  14728  repswswrd  14734  cshwcsh2id  14779  o1rlimmul  15563  dvdsabseq  16256  divalgb  16347  bezoutlem3  16483  cncongr1  16604  ncoprmlnprm  16664  difsqpwdvds  16820  lss1d  20574  pf1ind  21874  chfacfisf  22356  chfacfisfcpmat  22357  cayleyhamilton1  22394  txlm  23152  fmfnfmlem1  23458  blsscls2  24013  metcnpi3  24055  bcmono  26780  sletr  27261  upgrewlkle2  28863  redwlk  28929  crctcshwlkn0lem5  29068  wwlksnextwrd  29151  clwwlknonex2lem2  29361  ocnel  30551  atcvat2i  31640  atcvat4i  31650  dfon2lem5  34759  cgrxfr  35027  colinearxfr  35047  hfelhf  35153  isbasisrelowllem1  36236  isbasisrelowllem2  36237  finxpreclem6  36277  seqpo  36615  atlatle  38190  cvrexchlem  38290  cvrat2  38300  cvrat4  38314  pmapjoin  38723  onfrALTlem2  43307  onfrALTlem2VD  43650  eluzge0nn0  46020  elfz2z  46023  iccpartiltu  46090  iccpartigtl  46091  iccpartlt  46092  lighneal  46279  bgoldbtbnd  46477  tgoldbach  46485  cznnring  46854  ply1mulgsumlem2  47068  itsclc0  47457