Theorem expd 256

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-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  expdimp  257  pm3.3  259  syland  291  exp32  363  exp4c  366  exp4d  367  exp42  369  exp44  371  exp5c  374  impl  378  mpan2d  425  a2and  548  pm2.6dc  848  3impib  1180  exp5o  1205  biassdc  1374  exbir  1413  expcomd  1418  expdcom  1419  mopick  2078  ralrimivv  2516  mob2  2868  reuind  2893  difin  3318  reupick3  3366  suctr  4351  tfisi  4509  relop  4697  funcnvuni  5200  fnun  5237  mpteqb  5519  funfvima  5657  poxp  6137  nnmass  6391  supisoti  6905  axprecex  7712  ltnsym  7874  nn0lt2  9156  fzind  9190  fnn0ind  9191  btwnz  9194  lbzbi  9435  ledivge1le  9543  elfz0ubfz0  9933  elfzo0z  9992  fzofzim  9996  flqeqceilz  10122  leexp2r  10378  bernneq  10443  cau3lem  10918  climuni  11094  mulcn2  11113  dvdsabseq  11581  ndvdssub  11663  bezoutlemmain  11722  rplpwr  11751  algcvgblem  11766  euclemma  11860  basis2  12254  txcnp  12479  metcnp3  12719