Theorem expcomd 420

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  ancomsd  469  simplbi2comt  505  ralrimdva  3161  reupick  4281  pwssun  5537  ordelord  6364  tz7.7  6368  onelssex  6391  poxp  8103  smores2  8320  smoiun  8327  smogt  8333  tz7.49  8411  omsmolem  8622  mapxpen  9111  fodomfir  9268  f1dmvrnfibi  9281  suplub2  9404  epfrs  9683  r1sdom  9729  rankr1ai  9753  ficardom  9916  cardsdomel  9929  dfac5lem5  10080  cfsmolem  10224  cfcoflem  10226  axdc3lem2  10405  zorn2lem7  10456  genpn0  10958  reclem2pr  11003  supsrlem  11066  ltletr  11272  fzind  12668  rpneg  13024  xrltletr  13156  iccid  13391  ssfzoulel  13763  ssfzo12bi  13764  pfxccatin12lem2  14741  swrdccat  14745  repsdf2  14788  repswswrd  14794  cshwcsh2id  14838  o1rlimmul  15629  dvdsabseq  16330  divalgb  16421  bezoutlem3  16558  cncongr1  16684  ncoprmlnprm  16746  difsqpwdvds  16906  lss1d  21010  pf1ind  22398  chfacfisf  22894  chfacfisfcpmat  22895  cayleyhamilton1  22932  txlm  23688  fmfnfmlem1  23994  blsscls2  24544  metcnpi3  24586  bcmono  27318  lestr  27803  elreno2  28565  upgrewlkle2  29753  redwlk  29817  crctcshwlkn0lem5  29960  wwlksnextwrd  30043  clwwlknonex2lem2  30256  ocnel  31447  atcvat2i  32536  atcvat4i  32546  rankfilimb  35362  trssfir1om  35371  trssfir1omregs  35396  dfon2lem5  36099  cgrxfr  36369  colinearxfr  36389  hfelhf  36495  isbasisrelowllem1  37813  isbasisrelowllem2  37814  finxpreclem6  37854  seqpo  38210  atlatle  39908  cvrexchlem  40007  cvrat2  40017  cvrat4  40031  pmapjoin  40440  onfrALTlem2  45086  onfrALTlem2VD  45428  eluzge0nn0  47870  elfz2z  47873  iccpartiltu  47992  iccpartigtl  47993  iccpartlt  47994  lighneal  48184  bgoldbtbnd  48395  tgoldbach  48403  cznnring  48848  ply1mulgsumlem2  48973  itsclc0  49357