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  2999  reuind  3024  difin  3460  reupick3  3508  suctr  4544  tfisi  4711  relop  4907  funcnvuni  5427  fnun  5466  mpteqb  5770  funfvima  5920  riotaeqimp  6030  poxp  6430  nnmass  6722  rex2dom  7065  supisoti  7303  axprecex  8200  ltnsym  8364  nn0lt2  9665  fzind  9699  fnn0ind  9700  btwnz  9703  lbzbi  9954  ledivge1le  10065  elfz0ubfz0  10466  elfzo0z  10530  fzofzim  10534  flqeqceilz  10687  leexp2r  10962  bernneq  11030  swrdswrdlem  11404  swrdswrd  11405  wrd2ind  11423  swrdccatin1  11425  swrdccatin2  11429  pfxccatin12lem3  11432  cau3lem  11807  climuni  11986  mulcn2  12005  dvdsabseq  12541  ndvdssub  12624  bezoutlemmain  12702  rplpwr  12731  algcvgblem  12754  euclemma  12851  insubm  13719  grpinveu  13772  srgmulgass  14154  basis2  14962  txcnp  15185  metcnp3  15425  gausslemma2dlem3  15985  wlkl1loop  16402  wlk1walkdom  16403  uspgr2wlkeq  16409  eupth2lem3lem6fi  16515  bj-charfunr  16629