New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ex GIF version

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
StepHypRef Expression
1 df-an 360 . . 3 ((φ ψ) ↔ ¬ (φ → ¬ ψ))
2 exp.1 . . 3 ((φ ψ) → χ)
31, 2sylbir 204 . 2 (¬ (φ → ¬ ψ) → χ)
43expi 141 1 (φ → (ψχ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 358 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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  2507  dvelimdc  2509  pm2.61dane  2594  rgen2a  2680  ralimiaa  2688  ralimdaa  2691  ralrimiva  2697  ralrimdva  2704  ralrimivva  2706  ralrimdvv  2708  ralrimdvva  2709  reximdva  2726  rexlimiva  2733  rexlimdva  2738  rexlimdvva  2745  ralcom2  2775  2gencl  2888  vtocldf  2906  spcimdv  2936  rspct  2948  eqvinc  2966  ceqex  2969  reu6  3025  eqreu  3028  2rmorex  3040  2reu5  3044  sbciedf  3081  rmob  3134  csbiebt  3172  csbiedf  3173  sspsstr  3374  psssstr  3375  reupick  3539  reximdva0  3561  ssn0  3583  uneqdifeq  3638  r19.2zb  3640  dfnfc2  3909  intssuni  3948  unissint  3950  intab  3956  uniintsn  3963  iineq2d  3989  ssiun2  4009  pwadjoin  4119  opkthg  4131  iotaval  4350  iota2df  4365  nnsucelr  4428  nndisjeq  4429  preaddccan2  4455  ltfinirr  4457  ltfintr  4459  ltfinasym  4460  ltfintri  4466  lenltfin  4469  ssfin  4470  vfinnc  4471  ncfineleq  4477  ncfinraise  4481  ncfinlower  4483  nnpw1ex  4484  tfin11  4493  tfinsuc  4498  tfinltfinlem1  4500  tfinltfin  4501  evenodddisj  4516  eventfin  4517  oddtfin  4518  nnadjoin  4520  nnpweq  4523  sfin112  4529  sfintfin  4532  tfinnn  4534  sfin111  4536  spfininduct  4540  vfintle  4546  vfinspsslem1  4550  vfinspclt  4552  vinf  4555  nulnnn  4556  phi11lem1  4595  0cnelphi  4597  copsexg  4607  copsex2t  4608  2optocl  4839  ssxpb  5055  imadif  5171  2elresin  5194  feu  5242  f1oun  5304  tz6.12-1  5344  funbrfv  5356  dffn5  5363  fnrnfv  5364  funfv  5375  fvopab4t  5385  eqfnfv  5392  fvimacnv  5403  funimass3  5404  elpreima  5407  fnasrn  5417  dffo5  5424  ffvresb  5431  fsn  5432  funfvima  5459  funfvima2  5460  isotr  5495  oprabid  5550  ovidi  5594  ovg  5601  mpteq2da  5666  fmpt  5692  fvmptss  5705  fvmptf  5722  clos1basesuc  5882  ertr  5954  erref  5959  erdisj  5972  2ecoptocl  5997  unen  6048  enadjlem1  6059  enadj  6060  enmap2lem5  6067  enmap1lem5  6073  enprmaplem5  6080  nenpw1pwlem2  6085  eqncg  6126  ncdisjun  6136  peano4nc  6150  eqtc  6161  nntccl  6170  elce  6175  fce  6188  sbthlem3  6205  sbth  6206  leconnnc  6218  dflec3  6221  ce2le  6233  ce0tb  6238  nclenn  6249  ncslemuc  6255  nnltp1c  6262  addccan2nc  6265  lecadd2  6266  nmembers1lem2  6269  nnc3n3p1  6278  spacind  6287  spacis  6288  nchoicelem6  6294  nchoicelem9  6297  nchoicelem12  6300  nchoicelem14  6302  nchoicelem15  6303  nchoicelem17  6305  nchoice  6308  fnfreclem3  6319  fnfrec  6320
 Copyright terms: Public domain W3C validator