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  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  4564  tfisi  4732  relop  4928  funcnvuni  5448  fnun  5487  mpteqb  5793  funfvima  5944  riotaeqimp  6057  poxp  6462  nnmass  6754  rex2dom  7104  supisoti  7344  axprecex  8241  ltnsym  8405  nn0lt2  9710  fzind  9744  fnn0ind  9745  btwnz  9748  lbzbi  9999  ledivge1le  10110  elfz0ubfz0  10515  elfzo0z  10579  fzofzim  10583  flqeqceilz  10738  leexp2r  11013  bernneq  11081  swrdswrdlem  11459  swrdswrd  11460  wrd2ind  11478  swrdccatin1  11480  swrdccatin2  11484  pfxccatin12lem3  11487  cau3lem  11863  climuni  12042  mulcn2  12061  dvdsabseq  12597  ndvdssub  12680  bezoutlemmain  12758  rplpwr  12787  algcvgblem  12810  euclemma  12907  insubm  13775  grpinveu  13826  srgmulgass  14276  basis2  15132  txcnp  15355  metcnp3  15595  gausslemma2dlem3  16165  wlkl1loop  16582  wlk1walkdom  16583  uspgr2wlkeq  16589  eupth2lem3lem6fi  16695  lealltlt2  16735  bj-charfunr  16819