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  2157  ralrimivv  2612  mob2  2985  reuind  3010  difin  3443  reupick3  3491  suctr  4520  tfisi  4687  relop  4882  funcnvuni  5401  fnun  5440  mpteqb  5740  funfvima  5891  riotaeqimp  6001  poxp  6402  nnmass  6660  rex2dom  7001  supisoti  7214  axprecex  8105  ltnsym  8270  nn0lt2  9566  fzind  9600  fnn0ind  9601  btwnz  9604  lbzbi  9855  ledivge1le  9966  elfz0ubfz0  10365  elfzo0z  10429  fzofzim  10433  flqeqceilz  10586  leexp2r  10861  bernneq  10928  swrdswrdlem  11294  swrdswrd  11295  wrd2ind  11313  swrdccatin1  11315  swrdccatin2  11319  pfxccatin12lem3  11322  cau3lem  11697  climuni  11876  mulcn2  11895  dvdsabseq  12431  ndvdssub  12514  bezoutlemmain  12592  rplpwr  12621  algcvgblem  12644  euclemma  12741  insubm  13591  grpinveu  13644  srgmulgass  14026  basis2  14801  txcnp  15024  metcnp3  15264  gausslemma2dlem3  15821  wlkl1loop  16238  wlk1walkdom  16239  uspgr2wlkeq  16245  eupth2lem3lem6fi  16351  bj-charfunr  16465