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  864  3impib  1204  exp5o  1229  biassdc  1415  exbir  1457  expcomd  1462  expdcom  1463  mopick  2133  ralrimivv  2588  mob2  2954  reuind  2979  difin  3411  reupick3  3459  suctr  4472  tfisi  4639  relop  4832  funcnvuni  5348  fnun  5387  mpteqb  5677  funfvima  5823  poxp  6325  nnmass  6580  rex2dom  6917  supisoti  7119  axprecex  8000  ltnsym  8165  nn0lt2  9461  fzind  9495  fnn0ind  9496  btwnz  9499  lbzbi  9744  ledivge1le  9855  elfz0ubfz0  10254  elfzo0z  10315  fzofzim  10319  flqeqceilz  10470  leexp2r  10745  bernneq  10812  swrdswrdlem  11163  swrdswrd  11164  cau3lem  11469  climuni  11648  mulcn2  11667  dvdsabseq  12202  ndvdssub  12285  bezoutlemmain  12363  rplpwr  12392  algcvgblem  12415  euclemma  12512  insubm  13361  grpinveu  13414  srgmulgass  13795  basis2  14564  txcnp  14787  metcnp3  15027  gausslemma2dlem3  15584  bj-charfunr  15820