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  2984  reuind  3009  difin  3442  reupick3  3490  suctr  4516  tfisi  4683  relop  4878  funcnvuni  5396  fnun  5435  mpteqb  5733  funfvima  5881  riotaeqimp  5991  poxp  6392  nnmass  6650  rex2dom  6991  supisoti  7203  axprecex  8093  ltnsym  8258  nn0lt2  9554  fzind  9588  fnn0ind  9589  btwnz  9592  lbzbi  9843  ledivge1le  9954  elfz0ubfz0  10353  elfzo0z  10416  fzofzim  10420  flqeqceilz  10573  leexp2r  10848  bernneq  10915  swrdswrdlem  11278  swrdswrd  11279  wrd2ind  11297  swrdccatin1  11299  swrdccatin2  11303  pfxccatin12lem3  11306  cau3lem  11668  climuni  11847  mulcn2  11866  dvdsabseq  12401  ndvdssub  12484  bezoutlemmain  12562  rplpwr  12591  algcvgblem  12614  euclemma  12711  insubm  13561  grpinveu  13614  srgmulgass  13995  basis2  14765  txcnp  14988  metcnp3  15228  gausslemma2dlem3  15785  wlkl1loop  16169  wlk1walkdom  16170  uspgr2wlkeq  16176  bj-charfunr  16355