Theorem ex 423

Description: Exportation inference. (This theorem used to be labeled "exp" but was changed to "ex" so as not to conflict with the math token "exp", per the June 2006 Metamath spec change.) A translation of natural deduction rule → I (→ introduction), see natded in set.mm. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)

Hypothesis

Ref	Expression
exp.1	⊢ ((φ ∧ ψ) → χ)

Assertion

Ref	Expression
ex	⊢ (φ → (ψ → χ))

Proof of Theorem ex

Step	Hyp	Ref	Expression
1		df-an 360	. . 3 ⊢ ((φ ∧ ψ) ↔ ¬ (φ → ¬ ψ))
2		exp.1	. . 3 ⊢ ((φ ∧ ψ) → χ)
3	1, 2	sylbir 204	. 2 ⊢ (¬ (φ → ¬ ψ) → χ)
4	3	expi 141	1 ⊢ (φ → (ψ → χ))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  expcom  424  exp3a  425  impancom  427  pm2.01da  429  pm2.18da  430  pm3.2  434  jao  498  pm2.65da  559  expimpd  586  exp31  587  exp32  588  exp4b  590  exp41  593  exp43  595  exp53  600  impr  602  simplbi2  608  pm5.32da  622  anidms  626  mtand  640  syl2anc  642  pm5.74da  668  imdistanda  674  jaoian  759  jaodan  760  pm2.61ian  765  pm2.61dan  766  impbida  805  anim12dan  810  pm5.21nd  868  ecase  908  prlem1  928  pm3.2an3  1131  3jcad  1133  3impia  1148  3an1rs  1163  3exp1  1167  3exp2  1169  exp520  1172  syl3anl2  1231  3jaoian  1247  3jaodan  1248  mp3anl1  1271  mp3anl2  1272  mp3anl3  1273  inegd  1333  alanimi  1562  exlimddv  1638  nfimdOLD  1809  exlimdd  1889  sbequ1  1918  ax12  1935  dvelimh  1964  nfald2  1972  spimed  1977  equveli  1988  ax11v2  1992  cbvaldva  2010  cbvexdva  2011  sbiedv  2037  sbequi  2059  nfsb4t  2080  dvelimdf  2082  sbcom  2089  sbcom2  2114  sbal1  2126  dvelimALT  2133  ax12from12o  2156  dvelimf-o  2180  ax11indi  2196  ax11inda  2200  ax11v2-o  2201  eupickbi  2270  moexex  2273  nfabd2  2508  dvelimdc  2510  pm2.61dane  2595  rgen2a  2681  ralimiaa  2689  ralimdaa  2692  ralrimiva  2698  ralrimdva  2705  ralrimivva  2707  ralrimdvv  2709  ralrimdvva  2710  reximdva  2727  rexlimiva  2734  rexlimdva  2739  rexlimdvva  2746  ralcom2  2776  2gencl  2889  vtocldf  2907  spcimdv  2937  rspct  2949  eqvinc  2967  ceqex  2970  reu6  3026  eqreu  3029  2rmorex  3041  2reu5  3045  sbciedf  3082  rmob  3135  csbiebt  3173  csbiedf  3174  sspsstr  3375  psssstr  3376  reupick  3540  reximdva0  3562  ssn0  3584  uneqdifeq  3639  r19.2zb  3641  dfnfc2  3910  intssuni  3949  unissint  3951  intab  3957  uniintsn  3964  iineq2d  3990  ssiun2  4010  pwadjoin  4120  opkthg  4132  iotaval  4351  iota2df  4366  nnsucelr  4429  nndisjeq  4430  preaddccan2  4456  ltfinirr  4458  ltfintr  4460  ltfinasym  4461  ltfintri  4467  lenltfin  4470  ssfin  4471  vfinnc  4472  ncfineleq  4478  ncfinraise  4482  ncfinlower  4484  nnpw1ex  4485  tfin11  4494  tfinsuc  4499  tfinltfinlem1  4501  tfinltfin  4502  evenodddisj  4517  eventfin  4518  oddtfin  4519  nnadjoin  4521  nnpweq  4524  sfin112  4530  sfintfin  4533  tfinnn  4535  sfin111  4537  spfininduct  4541  vfintle  4547  vfinspsslem1  4551  vfinspclt  4553  vinf  4556  nulnnn  4557  phi11lem1  4596  0cnelphi  4598  copsexg  4608  copsex2t  4609  2optocl  4840  ssxpb  5056  imadif  5172  2elresin  5195  feu  5243  f1oun  5305  tz6.12-1  5345  funbrfv  5357  dffn5  5364  fnrnfv  5365  funfv  5376  fvopab4t  5386  eqfnfv  5393  fvimacnv  5404  funimass3  5405  elpreima  5408  fnasrn  5418  dffo5  5425  ffvresb  5432  fsn  5433  funfvima  5460  funfvima2  5461  isotr  5496  oprabid  5551  ovidi  5595  ovg  5602  mpteq2da  5667  fmpt  5693  fvmptss  5706  fvmptf  5723  clos1basesuc  5883  ertr  5955  erref  5960  erdisj  5973  2ecoptocl  5998  unen  6049  enadjlem1  6060  enadj  6061  enmap2lem5  6068  enmap1lem5  6074  enprmaplem5  6081  nenpw1pwlem2  6086  eqncg  6127  ncdisjun  6137  peano4nc  6151  eqtc  6162  nntccl  6171  elce  6176  fce  6189  sbthlem3  6206  sbth  6207  leconnnc  6219  dflec3  6222  ce2le  6234  ce0tb  6239  nclenn  6250  ncslemuc  6256  nnltp1c  6263  addccan2nc  6266  lecadd2  6267  nmembers1lem2  6270  nnc3n3p1  6279  spacind  6288  spacis  6289  nchoicelem6  6295  nchoicelem9  6298  nchoicelem12  6301  nchoicelem14  6303  nchoicelem15  6304  nchoicelem17  6306  nchoice  6309  fnfreclem3  6320  fnfrec  6321