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  3400  reupick3  3448  suctr  4456  tfisi  4623  relop  4816  funcnvuni  5327  fnun  5364  mpteqb  5652  funfvima  5794  poxp  6290  nnmass  6545  supisoti  7076  axprecex  7947  ltnsym  8112  nn0lt2  9407  fzind  9441  fnn0ind  9442  btwnz  9445  lbzbi  9690  ledivge1le  9801  elfz0ubfz0  10200  elfzo0z  10260  fzofzim  10264  flqeqceilz  10410  leexp2r  10685  bernneq  10752  cau3lem  11279  climuni  11458  mulcn2  11477  dvdsabseq  12012  ndvdssub  12095  bezoutlemmain  12165  rplpwr  12194  algcvgblem  12217  euclemma  12314  insubm  13117  grpinveu  13170  srgmulgass  13545  basis2  14284  txcnp  14507  metcnp3  14747  gausslemma2dlem3  15304  bj-charfunr  15456