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  1203  exp5o  1228  biassdc  1406  exbir  1447  expcomd  1452  expdcom  1453  mopick  2123  ralrimivv  2578  mob2  2944  reuind  2969  difin  3401  reupick3  3449  suctr  4457  tfisi  4624  relop  4817  funcnvuni  5328  fnun  5367  mpteqb  5655  funfvima  5797  poxp  6299  nnmass  6554  supisoti  7085  axprecex  7966  ltnsym  8131  nn0lt2  9426  fzind  9460  fnn0ind  9461  btwnz  9464  lbzbi  9709  ledivge1le  9820  elfz0ubfz0  10219  elfzo0z  10279  fzofzim  10283  flqeqceilz  10429  leexp2r  10704  bernneq  10771  cau3lem  11298  climuni  11477  mulcn2  11496  dvdsabseq  12031  ndvdssub  12114  bezoutlemmain  12192  rplpwr  12221  algcvgblem  12244  euclemma  12341  insubm  13189  grpinveu  13242  srgmulgass  13623  basis2  14370  txcnp  14593  metcnp3  14833  gausslemma2dlem3  15390  bj-charfunr  15542