Theorem expcomd 422

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ancomsd  471  simplbi2comt  507  ralrimdva  3168  reupick  4285  pwssun  5558  ordelord  6389  tz7.7  6393  onelssex  6417  poxp  8133  smores2  8350  smoiun  8357  smogt  8363  tz7.49  8441  omsmolem  8652  mapxpen  9141  fodomfir  9297  f1dmvrnfibi  9308  suplub2  9431  epfrs  9710  r1sdom  9756  rankr1ai  9780  ficardom  9966  cardsdomel  9979  dfac5lem5  10130  cfsmolem  10272  cfcoflem  10274  axdc3lem2  10453  zorn2lem7  10504  genpn0  11006  reclem2pr  11051  supsrlem  11114  ltletr  11320  fzind  12712  rpneg  13068  xrltletr  13200  iccid  13435  ssfzoulel  13808  ssfzo12bi  13809  pfxccatin12lem2  14792  swrdccat  14796  repsdf2  14841  repswswrd  14847  cshwcsh2id  14891  o1rlimmul  15696  dvdsabseq  16396  divalgb  16487  bezoutlem3  16624  cncongr1  16750  ncoprmlnprm  16812  difsqpwdvds  16972  lss1d  21121  pf1ind  22552  chfacfisf  23048  chfacfisfcpmat  23049  cayleyhamilton1  23086  txlm  23842  fmfnfmlem1  24148  blsscls2  24698  metcnpi3  24740  bcmono  27478  lestr  27963  elreno2  28725  upgrewlkle2  29993  redwlk  30057  crctcshwlkn0lem5  30200  wwlksnextwrd  30283  clwwlknonex2lem2  30496  ocnel  31687  atcvat2i  32776  atcvat4i  32786  rankfilimb  35521  trssfir1om  35532  trssfir1omregs  35573  dfon2lem5  36298  cgrxfr  36568  colinearxfr  36588  hfelhf  36694  isbasisrelowllem1  38042  isbasisrelowllem2  38043  finxpreclem6  38083  seqpo  38439  atlatle  40135  cvrexchlem  40234  cvrat2  40244  cvrat4  40258  pmapjoin  40667  onfrALTlem2  45296  onfrALTlem2VD  45638  eluzge0nn0  48090  elfz2z  48093  iccpartiltu  48212  iccpartigtl  48213  iccpartlt  48214  lighneal  48404  bgoldbtbnd  48615  tgoldbach  48623  cznnring  49068  ply1mulgsumlem2  49208  itsclc0  49592