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  558  pm2.6dc  866  3impib  1206  exp5o  1231  biassdc  1417  exbir  1459  expcomd  1464  expdcom  1465  mopick  2136  ralrimivv  2591  mob2  2963  reuind  2988  difin  3421  reupick3  3469  suctr  4489  tfisi  4656  relop  4849  funcnvuni  5366  fnun  5405  mpteqb  5698  funfvima  5844  riotaeqimp  5952  poxp  6348  nnmass  6603  rex2dom  6941  supisoti  7145  axprecex  8035  ltnsym  8200  nn0lt2  9496  fzind  9530  fnn0ind  9531  btwnz  9534  lbzbi  9779  ledivge1le  9890  elfz0ubfz0  10289  elfzo0z  10352  fzofzim  10356  flqeqceilz  10507  leexp2r  10782  bernneq  10849  swrdswrdlem  11202  swrdswrd  11203  wrd2ind  11221  swrdccatin1  11223  swrdccatin2  11227  pfxccatin12lem3  11230  cau3lem  11591  climuni  11770  mulcn2  11789  dvdsabseq  12324  ndvdssub  12407  bezoutlemmain  12485  rplpwr  12514  algcvgblem  12537  euclemma  12634  insubm  13484  grpinveu  13537  srgmulgass  13918  basis2  14687  txcnp  14910  metcnp3  15150  gausslemma2dlem3  15707  bj-charfunr  16083