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  867  3impib  1225  exp5o  1250  biassdc  1437  exbir  1479  expcomd  1484  expdcom  1485  mopick  2156  ralrimivv  2611  mob2  2983  reuind  3008  difin  3441  reupick3  3489  suctr  4512  tfisi  4679  relop  4872  funcnvuni  5390  fnun  5429  mpteqb  5727  funfvima  5875  riotaeqimp  5985  poxp  6384  nnmass  6641  rex2dom  6979  supisoti  7185  axprecex  8075  ltnsym  8240  nn0lt2  9536  fzind  9570  fnn0ind  9571  btwnz  9574  lbzbi  9819  ledivge1le  9930  elfz0ubfz0  10329  elfzo0z  10392  fzofzim  10396  flqeqceilz  10548  leexp2r  10823  bernneq  10890  swrdswrdlem  11244  swrdswrd  11245  wrd2ind  11263  swrdccatin1  11265  swrdccatin2  11269  pfxccatin12lem3  11272  cau3lem  11633  climuni  11812  mulcn2  11831  dvdsabseq  12366  ndvdssub  12449  bezoutlemmain  12527  rplpwr  12556  algcvgblem  12579  euclemma  12676  insubm  13526  grpinveu  13579  srgmulgass  13960  basis2  14730  txcnp  14953  metcnp3  15193  gausslemma2dlem3  15750  wlkl1loop  16079  wlk1walkdom  16080  uspgr2wlkeq  16086  bj-charfunr  16197