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  4513  tfisi  4680  relop  4875  funcnvuni  5393  fnun  5432  mpteqb  5730  funfvima  5878  riotaeqimp  5988  poxp  6389  nnmass  6646  rex2dom  6984  supisoti  7193  axprecex  8083  ltnsym  8248  nn0lt2  9544  fzind  9578  fnn0ind  9579  btwnz  9582  lbzbi  9828  ledivge1le  9939  elfz0ubfz0  10338  elfzo0z  10401  fzofzim  10405  flqeqceilz  10557  leexp2r  10832  bernneq  10899  swrdswrdlem  11257  swrdswrd  11258  wrd2ind  11276  swrdccatin1  11278  swrdccatin2  11282  pfxccatin12lem3  11285  cau3lem  11646  climuni  11825  mulcn2  11844  dvdsabseq  12379  ndvdssub  12462  bezoutlemmain  12540  rplpwr  12569  algcvgblem  12592  euclemma  12689  insubm  13539  grpinveu  13592  srgmulgass  13973  basis2  14743  txcnp  14966  metcnp3  15206  gausslemma2dlem3  15763  wlkl1loop  16130  wlk1walkdom  16131  uspgr2wlkeq  16137  bj-charfunr  16282