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  862  3impib  1201  exp5o  1226  biassdc  1395  exbir  1436  expcomd  1441  expdcom  1442  mopick  2104  ralrimivv  2558  mob2  2917  reuind  2942  difin  3372  reupick3  3420  suctr  4421  tfisi  4586  relop  4777  funcnvuni  5285  fnun  5322  mpteqb  5606  funfvima  5748  poxp  6232  nnmass  6487  supisoti  7008  axprecex  7878  ltnsym  8042  nn0lt2  9333  fzind  9367  fnn0ind  9368  btwnz  9371  lbzbi  9615  ledivge1le  9725  elfz0ubfz0  10124  elfzo0z  10183  fzofzim  10187  flqeqceilz  10317  leexp2r  10573  bernneq  10640  cau3lem  11122  climuni  11300  mulcn2  11319  dvdsabseq  11852  ndvdssub  11934  bezoutlemmain  11998  rplpwr  12027  algcvgblem  12048  euclemma  12145  insubm  12871  grpinveu  12910  srgmulgass  13170  basis2  13518  txcnp  13741  metcnp3  13981  bj-charfunr  14532