Theorem expd 255

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 114	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
4	3	com3r 79	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  expdimp  256  pm3.3  258  syland  288  exp32  358  exp4c  361  exp4d  362  exp42  364  exp44  366  exp5c  369  impl  373  mpan2d  420  a2and  526  pm2.6dc  798  3impib  1142  exp5o  1163  biassdc  1332  exbir  1371  expcomd  1376  expdcom  1377  mopick  2027  ralrimivv  2455  mob2  2796  reuind  2821  difin  3237  reupick3  3285  suctr  4257  tfisi  4415  relop  4599  funcnvuni  5096  fnun  5133  mpteqb  5406  funfvima  5540  poxp  6011  nnmass  6262  supisoti  6759  axprecex  7476  ltnsym  7632  nn0lt2  8889  fzind  8922  fnn0ind  8923  btwnz  8926  lbzbi  9162  ledivge1le  9264  elfz0ubfz0  9597  elfzo0z  9656  fzofzim  9660  flqeqceilz  9786  leexp2r  10070  bernneq  10135  cau3lem  10608  climuni  10742  mulcn2  10762  dvdsabseq  11187  ndvdssub  11269  bezoutlemmain  11326  rplpwr  11355  algcvgblem  11370  euclemma  11464  basis2  11807