Theorem expd 254

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

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  expdimp  255  pm3.3  257  syland  287  exp32  357  exp4c  360  exp4d  361  exp42  363  exp44  365  exp5c  368  impl  372  mpan2d  418  pm2.6dc  792  3impib  1136  exp5o  1157  biassdc  1326  exbir  1365  expcomd  1370  expdcom  1371  mopick  2019  ralrimivv  2442  mob2  2772  reuind  2795  difin  3201  reupick3  3249  suctr  4176  tfisi  4328  relop  4504  funcnvuni  4988  fnun  5025  mpteqb  5282  funfvima  5411  poxp  5873  nnmass  6089  supisoti  6423  axprecex  7046  ltnsym  7197  nn0lt2  8429  fzind  8462  fnn0ind  8463  btwnz  8466  lbzbi  8701  ledivge1le  8803  elfz0ubfz0  9136  elfzo0z  9193  fzofzim  9197  flqeqceilz  9320  leexp2r  9530  bernneq  9593  cau3lem  10000  climuni  10132  mulcn2  10151  dvdsabseq  10247  ndvdssub  10330  bezoutlemmain  10387  rplpwr  10416  algcvgblem  10431  euclemma  10525