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  862  3impib  1201  exp5o  1226  biassdc  1395  exbir  1436  expcomd  1441  expdcom  1442  mopick  2104  ralrimivv  2558  mob2  2918  reuind  2943  difin  3373  reupick3  3421  suctr  4422  tfisi  4587  relop  4778  funcnvuni  5286  fnun  5323  mpteqb  5607  funfvima  5749  poxp  6233  nnmass  6488  supisoti  7009  axprecex  7879  ltnsym  8043  nn0lt2  9334  fzind  9368  fnn0ind  9369  btwnz  9372  lbzbi  9616  ledivge1le  9726  elfz0ubfz0  10125  elfzo0z  10184  fzofzim  10188  flqeqceilz  10318  leexp2r  10574  bernneq  10641  cau3lem  11123  climuni  11301  mulcn2  11320  dvdsabseq  11853  ndvdssub  11935  bezoutlemmain  11999  rplpwr  12028  algcvgblem  12049  euclemma  12146  insubm  12872  grpinveu  12911  srgmulgass  13172  basis2  13551  txcnp  13774  metcnp3  14014  bj-charfunr  14565