Theorem expcomd 421

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ancomsd  470  simplbi2comt  506  ralrimdva  3165  reupick  4283  pwssun  5555  ordelord  6384  tz7.7  6388  onelssex  6412  poxp  8125  smores2  8342  smoiun  8349  smogt  8355  tz7.49  8433  omsmolem  8644  mapxpen  9132  fodomfir  9288  f1dmvrnfibi  9299  suplub2  9422  epfrs  9701  r1sdom  9747  rankr1ai  9771  ficardom  9948  cardsdomel  9961  dfac5lem5  10112  cfsmolem  10255  cfcoflem  10257  axdc3lem2  10436  zorn2lem7  10487  genpn0  10989  reclem2pr  11034  supsrlem  11097  ltletr  11303  fzind  12695  rpneg  13051  xrltletr  13183  iccid  13418  ssfzoulel  13791  ssfzo12bi  13792  pfxccatin12lem2  14770  swrdccat  14774  repsdf2  14817  repswswrd  14823  cshwcsh2id  14867  o1rlimmul  15672  dvdsabseq  16372  divalgb  16463  bezoutlem3  16600  cncongr1  16726  ncoprmlnprm  16788  difsqpwdvds  16948  lss1d  21065  pf1ind  22496  chfacfisf  22992  chfacfisfcpmat  22993  cayleyhamilton1  23030  txlm  23786  fmfnfmlem1  24092  blsscls2  24642  metcnpi3  24684  bcmono  27419  lestr  27904  elreno2  28666  upgrewlkle2  29934  redwlk  29998  crctcshwlkn0lem5  30141  wwlksnextwrd  30224  clwwlknonex2lem2  30437  ocnel  31628  atcvat2i  32717  atcvat4i  32727  rankfilimb  35474  trssfir1om  35485  trssfir1omregs  35527  dfon2lem5  36255  cgrxfr  36525  colinearxfr  36545  hfelhf  36651  isbasisrelowllem1  37979  isbasisrelowllem2  37980  finxpreclem6  38020  seqpo  38376  atlatle  40072  cvrexchlem  40171  cvrat2  40181  cvrat4  40195  pmapjoin  40604  onfrALTlem2  45235  onfrALTlem2VD  45577  eluzge0nn0  48026  elfz2z  48029  iccpartiltu  48148  iccpartigtl  48149  iccpartlt  48150  lighneal  48340  bgoldbtbnd  48551  tgoldbach  48559  cznnring  49004  ply1mulgsumlem2  49144  itsclc0  49528