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

Theorem imp 418
Description: Importation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
Hypothesis
Ref Expression
imp.1 (φ → (ψχ))
Assertion
Ref Expression
imp ((φ ψ) → χ)

Proof of Theorem imp
StepHypRef Expression
1 df-an 360 . 2 ((φ ψ) ↔ ¬ (φ → ¬ ψ))
2 imp.1 . . 3 (φ → (ψχ))
32impi 140 . 2 (¬ (φ → ¬ ψ) → χ)
41, 3sylbi 187 1 ((φ ψ) → χ)
Colors of variables: wff setvar class
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:  impcom  419  imp3a  420  imp31  421  imp32  422  expdimp  426  impancom  427  con3and  428  pm3.22  436  ancoms  439  simpl  443  simpr  447  adantr  451  biimpa  470  biimpar  471  biimpac  472  biimparc  473  pm3.33  568  pm3.34  569  pm3.35  570  pm5.31  571  imp4b  573  imp41  576  imp42  577  imp43  578  imp44  579  imp45  580  imp5g  583  expr  598  impac  604  sylan9  638  sylan9r  639  imdistani  671  jaoian  759  jaodan  760  anabsi5  790  anim12dan  810  pm5.21  831  pm3.43  832  orcanai  879  pm4.82  894  3jcad  1133  3expia  1153  3an1rs  1163  3imp1  1164  3imp2  1166  syl3anl2  1231  3jaoian  1247  3jaodan  1248  mp3anl1  1271  mp3anl2  1272  mp3anl3  1273  alanimi  1562  19.29  1596  nfimdOLD  1809  equs5a  1887  ax12olem3  1929  ax12  1935  dvelimv  1939  ax10  1944  nfeqf  1958  equs4  1959  dvelimh  1964  ax11v2  1992  ax11b  1995  equvin  2001  dfsb2  2055  dvelimdf  2082  sb5rf  2090  dvelimALT  2133  ax12from12o  2156  dvelimf-o  2180  ax11eq  2193  ax11el  2194  ax11indi  2196  ax11indalem  2197  ax11inda2ALT  2198  ax11inda  2200  ax11v2-o  2201  mopick  2266  moexex  2273  exists2  2294  eqrdav  2352  dvelimdc  2509  pm13.18  2588  nelne1  2605  nelne2  2606  ralrimdvv  2708  r19.21bi  2712  r19.26  2746  ralbi  2750  r19.29  2754  vtoclgft  2905  rspcva  2953  rspc2va  2962  elabgt  2982  eqeu  3007  mob2  3016  mob  3018  euind  3023  reu6  3025  reuind  3039  sbctt  3108  rspsbca  3125  csbexg  3146  sbcnestgf  3183  rspcsbela  3195  ssel2  3268  sselda  3273  sstr  3280  nssne1  3327  nssne2  3328  sspsstr  3374  psssstr  3375  neldif  3391  reuss2  3535  reupick  3539  reupick2  3541  reximdva0  3561  ssn0  3583  disjel  3597  ssdisj  3600  disjpss  3601  pssdifn0  3611  uneqdifeq  3638  dedth2h  3704  dedth4h  3706  absneu  3794  uniintsn  3963  dfiun2g  3999  ssofss  4076  opkthg  4131  pw1disj  4167  nncaddccl  4419  nnsucelr  4428  nndisjeq  4429  ncfinlower  4483  nnpw1ex  4484  tfinsuc  4498  tfinltfin  4501  evenoddnnnul  4514  eventfin  4517  oddtfin  4518  nnadjoin  4520  nnpweq  4523  sfindbl  4530  tfinnn  4534  sfinltfin  4535  nulnnn  4556  copsex2t  4608  nbrne1  4656  nbrne2  4657  vtoclr  4816  optocl  4838  funssres  5144  fununi  5160  funimass2  5170  fnun  5189  fco  5231  opelf  5235  f1oun  5304  fun11iun  5305  fv3  5341  fvelima  5369  fvun1  5379  dff3  5420  funfvima2  5460  isotr  5495  isoini  5497  ndmovg  5613  mpteq12f  5655  fvmpti  5699  fvmptf  5722  trtxp  5781  op1st2nd  5790  oqelins4  5794  qrpprod  5836  erth  5968  ectocld  5991  f1oeng  6032  fundmeng  6044  unen  6048  enprmaplem5  6080  nceleq  6149  peano4nc  6150  ce0ncpw1  6185  cecl  6186  sbthlem3  6205  lecponc  6213  leaddc1  6214  leconnnc  6218  dflec3  6221  taddc  6229  ce2le  6233  nclenn  6249  lemuc1  6253  ncslemuc  6255  nmembers1lem2  6269  nnc3n3p1  6278  spacind  6287  nchoicelem3  6291  nchoicelem12  6300  nchoicelem14  6302  nchoicelem15  6303  nchoicelem17  6305  nchoicelem19  6307  frecxp  6314  fnfreclem3  6319  fnfrec  6320
  Copyright terms: Public domain W3C validator