Theorem expcomd 419

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ancomsd  468  simplbi2comt  504  ralrimdva  3189  reupick  4287  pwssun  5456  ordelord  6213  tz7.7  6217  poxp  7822  smores2  7991  smoiun  7998  smogt  8004  tz7.49  8081  omsmolem  8280  mapxpen  8683  f1dmvrnfibi  8808  suplub2  8925  epfrs  9173  r1sdom  9203  rankr1ai  9227  ficardom  9390  cardsdomel  9403  dfac5lem5  9553  cfsmolem  9692  cfcoflem  9694  axdc3lem2  9873  zorn2lem7  9924  genpn0  10425  reclem2pr  10470  supsrlem  10533  ltletr  10732  fzind  12081  rpneg  12422  xrltletr  12551  iccid  12784  ssfzoulel  13132  ssfzo12bi  13133  pfxccatin12lem2  14093  swrdccat  14097  repsdf2  14140  repswswrd  14146  cshwcsh2id  14190  o1rlimmul  14975  dvdsabseq  15663  divalgb  15755  bezoutlem3  15889  cncongr1  16011  ncoprmlnprm  16068  difsqpwdvds  16223  lss1d  19735  pf1ind  20518  chfacfisf  21462  chfacfisfcpmat  21463  cayleyhamilton1  21500  txlm  22256  fmfnfmlem1  22562  blsscls2  23114  metcnpi3  23156  bcmono  25853  upgrewlkle2  27388  redwlk  27454  crctcshwlkn0lem5  27592  wwlksnextwrd  27675  clwwlknonex2lem2  27887  ocnel  29075  atcvat2i  30164  atcvat4i  30174  dfon2lem5  33032  sletr  33237  cgrxfr  33516  colinearxfr  33536  hfelhf  33642  isbasisrelowllem1  34639  isbasisrelowllem2  34640  finxpreclem6  34680  seqpo  35037  atlatle  36471  cvrexchlem  36570  cvrat2  36580  cvrat4  36594  pmapjoin  37003  onfrALTlem2  40929  onfrALTlem2VD  41272  eluzge0nn0  43561  elfz2z  43564  iccpartiltu  43631  iccpartigtl  43632  iccpartlt  43633  lighneal  43825  bgoldbtbnd  44023  tgoldbach  44031  cznnring  44276  ply1mulgsumlem2  44490  itsclc0  44807