Theorem expcomd 422

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ancomsd  471  simplbi2comt  507  ralrimdva  3166  reupick  4277  pwssun  5547  ordelord  6402  tz7.7  6406  onelssex  6430  poxp  8167  smores2  8390  smoiun  8397  smogt  8403  tz7.49  8483  omsmolem  8694  mapxpen  9190  fodomfir  9347  f1dmvrnfibi  9358  suplub2  9480  epfrs  9759  r1sdom  9808  rankr1ai  9833  hfelhfOLD  9943  ficardom  10069  cardsdomel  10082  dfac5lem5  10233  cfsmolem  10375  cfcoflem  10377  axdc3lem2  10556  zorn2lem7  10607  genpn0  11115  reclem2pr  11160  supsrlem  11223  ltletr  11429  fzind  12824  rpneg  13181  xrltletr  13313  iccid  13548  ssfzoulel  13922  ssfzo12bi  13923  pfxccatin12lem2  14908  swrdccat  14912  repsdf2  14957  repswswrd  14963  cshwcsh2id  15007  o1rlimmul  15815  dvdsabseq  16512  divalgb  16603  bezoutlem3  16743  cncongr1  16871  ncoprmlnprm  16933  difsqpwdvds  17094  lss1d  21268  pf1ind  22703  chfacfisf  23202  chfacfisfcpmat  23203  cayleyhamilton1  23240  txlm  23997  fmfnfmlem1  24303  blsscls2  24853  metcnpi3  24895  bcmono  27634  lestr  28149  elreno2  28911  upgrewlkle2  30217  redwlk  30281  crctcshwlkn0lem5  30433  wwlksnextwrd  30516  clwwlknonex2lem2  30729  ocnel  31930  atcvat2i  33019  atcvat4i  33029  rankfilimb  35812  trssfihf  35819  trssfihfregs  35904  dfon2lem5  36727  cgrxfr  36998  colinearxfr  37018  isbasisrelowllem1  38470  isbasisrelowllem2  38471  finxpreclem6  38511  seqpo  38873  atlatle  40569  cvrexchlem  40668  cvrat2  40678  cvrat4  40692  pmapjoin  41101  onfrALTlem2  45720  onfrALTlem2VD  46062  eluzge0nn0  48587  elfz2z  48590  iccpartiltu  48709  iccpartigtl  48710  iccpartlt  48711  lighneal  48901  bgoldbtbnd  49112  tgoldbach  49120  cznnring  49564  ply1mulgsumlem2  49704  itsclc0  50088