Theorem expd 258

Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.)

Hypothesis

Ref	Expression
exp3a.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
expd	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem expd

Step	Hyp	Ref	Expression
1		exp3a.1	. . . 4 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	com12 30	. . 3 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
3	2	ex 115	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
4	3	com3r 79	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  expdimp  259  pm3.3  261  syland  293  exp32  365  exp4c  368  exp4d  369  exp42  371  exp44  373  exp5c  376  impl  380  mpan2d  428  a2and  560  pm2.6dc  870  3impib  1228  exp5o  1253  biassdc  1440  exbir  1482  expcomd  1487  expdcom  1488  mopick  2159  ralrimivv  2623  mob2  2996  reuind  3021  difin  3457  reupick3  3505  suctr  4541  tfisi  4708  relop  4904  funcnvuni  5424  fnun  5463  mpteqb  5767  funfvima  5917  riotaeqimp  6027  poxp  6427  nnmass  6719  rex2dom  7062  supisoti  7300  axprecex  8191  ltnsym  8355  nn0lt2  9655  fzind  9689  fnn0ind  9690  btwnz  9693  lbzbi  9944  ledivge1le  10055  elfz0ubfz0  10455  elfzo0z  10519  fzofzim  10523  flqeqceilz  10676  leexp2r  10951  bernneq  11018  swrdswrdlem  11389  swrdswrd  11390  wrd2ind  11408  swrdccatin1  11410  swrdccatin2  11414  pfxccatin12lem3  11417  cau3lem  11792  climuni  11971  mulcn2  11990  dvdsabseq  12526  ndvdssub  12609  bezoutlemmain  12687  rplpwr  12716  algcvgblem  12739  euclemma  12836  insubm  13687  grpinveu  13740  srgmulgass  14122  basis2  14900  txcnp  15123  metcnp3  15363  gausslemma2dlem3  15923  wlkl1loop  16340  wlk1walkdom  16341  uspgr2wlkeq  16347  eupth2lem3lem6fi  16453  bj-charfunr  16567