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  2161  ralrimivv  2625  mob2  3000  reuind  3025  difin  3462  reupick3  3510  suctr  4547  tfisi  4714  relop  4910  funcnvuni  5430  fnun  5469  mpteqb  5773  funfvima  5923  riotaeqimp  6036  poxp  6441  nnmass  6733  rex2dom  7076  supisoti  7314  axprecex  8211  ltnsym  8375  nn0lt2  9680  fzind  9714  fnn0ind  9715  btwnz  9718  lbzbi  9969  ledivge1le  10080  elfz0ubfz0  10484  elfzo0z  10548  fzofzim  10552  flqeqceilz  10707  leexp2r  10982  bernneq  11050  swrdswrdlem  11424  swrdswrd  11425  wrd2ind  11443  swrdccatin1  11445  swrdccatin2  11449  pfxccatin12lem3  11452  cau3lem  11827  climuni  12006  mulcn2  12025  dvdsabseq  12561  ndvdssub  12644  bezoutlemmain  12722  rplpwr  12751  algcvgblem  12774  euclemma  12871  insubm  13743  grpinveu  13796  srgmulgass  14235  basis2  15042  txcnp  15265  metcnp3  15505  gausslemma2dlem3  16065  wlkl1loop  16482  wlk1walkdom  16483  uspgr2wlkeq  16489  eupth2lem3lem6fi  16595  lealltlt2  16635  bj-charfunr  16719