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  2917  reuind  2942  difin  3372  reupick3  3420  suctr  4419  tfisi  4584  relop  4774  funcnvuni  5282  fnun  5319  mpteqb  5603  funfvima  5744  poxp  6228  nnmass  6483  supisoti  7004  axprecex  7874  ltnsym  8037  nn0lt2  9328  fzind  9362  fnn0ind  9363  btwnz  9366  lbzbi  9610  ledivge1le  9720  elfz0ubfz0  10118  elfzo0z  10177  fzofzim  10181  flqeqceilz  10311  leexp2r  10567  bernneq  10633  cau3lem  11114  climuni  11292  mulcn2  11311  dvdsabseq  11843  ndvdssub  11925  bezoutlemmain  11989  rplpwr  12018  algcvgblem  12039  euclemma  12136  insubm  12800  grpinveu  12839  srgmulgass  13072  basis2  13328  txcnp  13553  metcnp3  13793  bj-charfunr  14333