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  4284  pwssun  5544  ordelord  6372  tz7.7  6376  onelssex  6399  poxp  8112  smores2  8329  smoiun  8336  smogt  8342  tz7.49  8420  omsmolem  8631  mapxpen  9119  fodomfir  9275  f1dmvrnfibi  9286  suplub2  9409  epfrs  9688  r1sdom  9734  rankr1ai  9758  ficardom  9935  cardsdomel  9948  dfac5lem5  10099  cfsmolem  10242  cfcoflem  10244  axdc3lem2  10423  zorn2lem7  10474  genpn0  10976  reclem2pr  11021  supsrlem  11084  ltletr  11290  fzind  12685  rpneg  13041  xrltletr  13173  iccid  13408  ssfzoulel  13780  ssfzo12bi  13781  pfxccatin12lem2  14758  swrdccat  14762  repsdf2  14805  repswswrd  14811  cshwcsh2id  14855  o1rlimmul  15660  dvdsabseq  16361  divalgb  16452  bezoutlem3  16589  cncongr1  16715  ncoprmlnprm  16777  difsqpwdvds  16937  lss1d  21053  pf1ind  22476  chfacfisf  22972  chfacfisfcpmat  22973  cayleyhamilton1  23010  txlm  23766  fmfnfmlem1  24072  blsscls2  24622  metcnpi3  24664  bcmono  27399  lestr  27884  elreno2  28646  upgrewlkle2  29865  redwlk  29929  crctcshwlkn0lem5  30072  wwlksnextwrd  30155  clwwlknonex2lem2  30368  ocnel  31559  atcvat2i  32648  atcvat4i  32658  rankfilimb  35410  trssfir1om  35419  trssfir1omregs  35444  dfon2lem5  36148  cgrxfr  36418  colinearxfr  36438  hfelhf  36544  isbasisrelowllem1  37861  isbasisrelowllem2  37862  finxpreclem6  37902  seqpo  38258  atlatle  39956  cvrexchlem  40055  cvrat2  40065  cvrat4  40079  pmapjoin  40488  onfrALTlem2  45120  onfrALTlem2VD  45462  eluzge0nn0  47904  elfz2z  47907  iccpartiltu  48026  iccpartigtl  48027  iccpartlt  48028  lighneal  48218  bgoldbtbnd  48429  tgoldbach  48437  cznnring  48882  ply1mulgsumlem2  49018  itsclc0  49402