Theorem expcomd 406

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

Syntax hints:   → wi 4   ∧ wa 384

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

This theorem is referenced by:  simplbi2comt  495  ralrimdva  3116  reupick  4075  pwssun  5181  ordelord  5930  tz7.7  5934  poxp  7491  smores2  7655  smoiun  7662  smogt  7668  tz7.49  7744  omsmolem  7938  mapxpen  8333  f1dmvrnfibi  8457  suplub2  8574  epfrs  8822  r1sdom  8852  rankr1ai  8876  ficardom  9038  cardsdomel  9051  dfac5lem5  9201  cfsmolem  9345  cfcoflem  9347  axdc3lem2  9526  zorn2lem7  9577  genpn0  10078  reclem2pr  10123  supsrlem  10185  ltletr  10383  fzind  11722  rpneg  12061  xrltletr  12190  iccid  12422  ssfzoulel  12770  ssfzo12bi  12771  pfxccatin12lem2  13736  swrdccatin12lem2OLD  13737  swrdccat  13743  swrdccatOLD  13744  repsdf2  13802  repswswrd  13808  cshwcsh2id  13859  o1rlimmul  14636  dvdsabseq  15322  divalgb  15411  bezoutlem3  15541  cncongr1  15663  ncoprmlnprm  15717  difsqpwdvds  15872  lss1d  19235  pf1ind  19992  chfacfisf  20938  chfacfisfcpmat  20939  cayleyhamilton1  20976  txlm  21731  fmfnfmlem1  22037  blsscls2  22588  metcnpi3  22630  bcmono  25293  upgrewlkle2  26793  redwlk  26860  crctcshwlkn0lem5  26998  wwlksnextwrd  27097  clwwlknonex2lem2  27340  ocnel  28548  atcvat2i  29637  atcvat4i  29647  dfon2lem5  32067  sletr  32259  cgrxfr  32538  colinearxfr  32558  hfelhf  32664  isbasisrelowllem1  33568  isbasisrelowllem2  33569  finxpreclem6  33598  seqpo  33897  atlatle  35208  cvrexchlem  35307  cvrat2  35317  cvrat4  35331  pmapjoin  35740  onfrALTlem2  39356  onfrALTlem2VD  39709  eluzge0nn0  41988  elfz2z  41991  iccpartiltu  42024  iccpartigtl  42025  iccpartlt  42026  lighneal  42136  bgoldbtbnd  42305  tgoldbach  42313  cznnring  42557  ply1mulgsumlem2  42776