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  3138  reupick  4270  pwssun  5516  ordelord  6339  tz7.7  6343  onelssex  6366  poxp  8071  smores2  8287  smoiun  8294  smogt  8300  tz7.49  8377  omsmolem  8586  mapxpen  9074  fodomfir  9231  f1dmvrnfibi  9244  suplub2  9367  epfrs  9643  r1sdom  9689  rankr1ai  9713  ficardom  9876  cardsdomel  9889  dfac5lem5  10040  cfsmolem  10183  cfcoflem  10185  axdc3lem2  10364  zorn2lem7  10415  genpn0  10917  reclem2pr  10962  supsrlem  11025  ltletr  11229  fzind  12618  rpneg  12967  xrltletr  13099  iccid  13334  ssfzoulel  13706  ssfzo12bi  13707  pfxccatin12lem2  14684  swrdccat  14688  repsdf2  14731  repswswrd  14737  cshwcsh2id  14781  o1rlimmul  15572  dvdsabseq  16273  divalgb  16364  bezoutlem3  16501  cncongr1  16627  ncoprmlnprm  16689  difsqpwdvds  16849  lss1d  20949  pf1ind  22330  chfacfisf  22829  chfacfisfcpmat  22830  cayleyhamilton1  22867  txlm  23623  fmfnfmlem1  23929  blsscls2  24479  metcnpi3  24521  bcmono  27254  lestr  27740  elreno2  28501  upgrewlkle2  29690  redwlk  29754  crctcshwlkn0lem5  29897  wwlksnextwrd  29980  clwwlknonex2lem2  30193  ocnel  31384  atcvat2i  32473  atcvat4i  32483  rankfilimb  35261  trssfir1om  35271  trssfir1omregs  35296  dfon2lem5  35983  cgrxfr  36253  colinearxfr  36273  hfelhf  36379  isbasisrelowllem1  37685  isbasisrelowllem2  37686  finxpreclem6  37726  seqpo  38082  atlatle  39780  cvrexchlem  39879  cvrat2  39889  cvrat4  39903  pmapjoin  40312  onfrALTlem2  44991  onfrALTlem2VD  45333  eluzge0nn0  47772  elfz2z  47775  iccpartiltu  47894  iccpartigtl  47895  iccpartlt  47896  lighneal  48086  bgoldbtbnd  48297  tgoldbach  48305  cznnring  48750  ply1mulgsumlem2  48875  itsclc0  49259