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 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  expdimp  259  pm3.3  261  syland  293  exp32  365  exp4c  368  exp4d  369  exp42  371  exp44  373  exp5c  376  impl  380  mpan2d  432  a2and  564  pm2.6dc  874  3impib  1232  exp5o  1257  biassdc  1444  exbir  1486  expcomd  1491  expdcom  1492  mopick  2165  ralrimivv  2631  mob2  3006  reuind  3031  difin  3468  reupick3  3518  suctr  4568  tfisi  4736  relop  4932  funcnvuni  5453  fnun  5492  mpteqb  5799  funfvima  5953  riotaeqimp  6066  poxp  6472  nnmass  6764  rex2dom  7115  supisoti  7357  axprecex  8254  ltnsym  8418  nn0lt2  9739  fzind  9773  fnn0ind  9774  btwnz  9777  lbzbi  10033  ledivge1le  10145  elfz0ubfz0  10550  elfzo0z  10614  fzofzim  10618  flqeqceilz  10777  leexp2r  11052  bernneq  11120  swrdswrdlem  11499  swrdswrd  11500  wrd2ind  11518  swrdccatin1  11520  swrdccatin2  11524  pfxccatin12lem3  11527  cau3lem  11904  climuni  12085  mulcn2  12104  dvdsabseq  12640  ndvdssub  12723  bezoutlemmain  12801  rplpwr  12830  algcvgblem  12853  euclemma  12951  prmlem1a  13251  insubm  13852  grpinveu  13903  srgmulgass  14401  basis2  15286  txcnp  15509  metcnp3  15749  gausslemma2dlem3  16399  wlkl1loop  16816  wlk1walkdom  16817  uspgr2wlkeq  16823  eupth2lem3lem6fi  16929  lealltlt2  16969  bj-charfunr  17053