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  863  3impib  1202  exp5o  1227  biassdc  1405  exbir  1446  expcomd  1451  expdcom  1452  mopick  2114  ralrimivv  2568  mob2  2929  reuind  2954  difin  3384  reupick3  3432  suctr  4433  tfisi  4598  relop  4789  funcnvuni  5297  fnun  5334  mpteqb  5619  funfvima  5761  poxp  6246  nnmass  6501  supisoti  7022  axprecex  7892  ltnsym  8056  nn0lt2  9347  fzind  9381  fnn0ind  9382  btwnz  9385  lbzbi  9629  ledivge1le  9739  elfz0ubfz0  10138  elfzo0z  10197  fzofzim  10201  flqeqceilz  10331  leexp2r  10587  bernneq  10654  cau3lem  11136  climuni  11314  mulcn2  11333  dvdsabseq  11866  ndvdssub  11948  bezoutlemmain  12012  rplpwr  12041  algcvgblem  12062  euclemma  12159  insubm  12893  grpinveu  12934  srgmulgass  13236  basis2  13819  txcnp  14042  metcnp3  14282  bj-charfunr  14833