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  3132  reupick  4279  pwssun  5508  ordelord  6328  tz7.7  6332  onelssex  6355  poxp  8058  smores2  8274  smoiun  8281  smogt  8287  tz7.49  8364  omsmolem  8572  mapxpen  9056  fodomfir  9212  f1dmvrnfibi  9225  suplub2  9345  epfrs  9621  r1sdom  9664  rankr1ai  9688  ficardom  9851  cardsdomel  9864  dfac5lem5  10015  cfsmolem  10158  cfcoflem  10160  axdc3lem2  10339  zorn2lem7  10390  genpn0  10891  reclem2pr  10936  supsrlem  10999  ltletr  11202  fzind  12568  rpneg  12921  xrltletr  13053  iccid  13287  ssfzoulel  13657  ssfzo12bi  13658  pfxccatin12lem2  14635  swrdccat  14639  repsdf2  14682  repswswrd  14688  cshwcsh2id  14732  o1rlimmul  15523  dvdsabseq  16221  divalgb  16312  bezoutlem3  16449  cncongr1  16575  ncoprmlnprm  16636  difsqpwdvds  16796  lss1d  20894  pf1ind  22268  chfacfisf  22767  chfacfisfcpmat  22768  cayleyhamilton1  22805  txlm  23561  fmfnfmlem1  23867  blsscls2  24417  metcnpi3  24459  bcmono  27213  sletr  27695  upgrewlkle2  29583  redwlk  29647  crctcshwlkn0lem5  29790  wwlksnextwrd  29873  clwwlknonex2lem2  30083  ocnel  31273  atcvat2i  32362  atcvat4i  32372  trssfir1omregs  35120  dfon2lem5  35820  cgrxfr  36088  colinearxfr  36108  hfelhf  36214  isbasisrelowllem1  37388  isbasisrelowllem2  37389  finxpreclem6  37429  seqpo  37786  atlatle  39358  cvrexchlem  39457  cvrat2  39467  cvrat4  39481  pmapjoin  39890  onfrALTlem2  44578  onfrALTlem2VD  44920  eluzge0nn0  47342  elfz2z  47345  iccpartiltu  47452  iccpartigtl  47453  iccpartlt  47454  lighneal  47641  bgoldbtbnd  47839  tgoldbach  47847  cznnring  48292  ply1mulgsumlem2  48418  itsclc0  48802