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  869  3impib  1227  exp5o  1252  biassdc  1439  exbir  1481  expcomd  1486  expdcom  1487  mopick  2158  ralrimivv  2613  mob2  2986  reuind  3011  difin  3444  reupick3  3492  suctr  4518  tfisi  4685  relop  4880  funcnvuni  5399  fnun  5438  mpteqb  5737  funfvima  5886  riotaeqimp  5996  poxp  6397  nnmass  6655  rex2dom  6996  supisoti  7209  axprecex  8100  ltnsym  8265  nn0lt2  9561  fzind  9595  fnn0ind  9596  btwnz  9599  lbzbi  9850  ledivge1le  9961  elfz0ubfz0  10360  elfzo0z  10424  fzofzim  10428  flqeqceilz  10581  leexp2r  10856  bernneq  10923  swrdswrdlem  11286  swrdswrd  11287  wrd2ind  11305  swrdccatin1  11307  swrdccatin2  11311  pfxccatin12lem3  11314  cau3lem  11676  climuni  11855  mulcn2  11874  dvdsabseq  12410  ndvdssub  12493  bezoutlemmain  12571  rplpwr  12600  algcvgblem  12623  euclemma  12720  insubm  13570  grpinveu  13623  srgmulgass  14005  basis2  14775  txcnp  14998  metcnp3  15238  gausslemma2dlem3  15795  wlkl1loop  16212  wlk1walkdom  16213  uspgr2wlkeq  16219  eupth2lem3lem6fi  16325  bj-charfunr  16426