Theorem pm2.21 120

Description: From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. Its associated inference is pm2.21i 116. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 14-Sep-2012.)

Assertion

Ref	Expression
pm2.21	|- ( -. ph -> ( ph -> ps ) )

Proof of Theorem pm2.21

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( -. ph -> -. ph )
2	1	pm2.21d 118	1 |- ( -. ph -> ( ph -> ps ) )

Syntax hints:   -. wn 3   -> wi 4

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

This theorem is referenced by:  pm2.24  121  pm2.18  122  notnotr  125  simplim  163  jarl  175  orel2  398  pm2.42  598  pm4.82  969  pm5.71  977  cases2  993  dedlem0b  1001  dedlemb  1003  cad0  1556  meredith  1566  tbw-bijust  1623  tbw-negdf  1624  19.38  1766  19.35  1805  nfimdOLDOLD  1824  ax13dgen2  2015  ax13dgen4  2017  nfim1  2067  sbi2  2393  mo2v  2477  exmo  2495  2mo  2551  axin2  2591  nrexrmo  3163  elab3gf  3356  moeq3  3383  opthpr  4384  dfopif  4399  dvdemo1  4902  weniso  6604  0neqopab  6698  dfwe2  6981  ordunisuc2  7044  0mnnnnn0  11325  nn0ge2m1nn  11360  xrub  12142  injresinjlem  12588  fleqceilz  12653  addmodlteq  12745  fsuppmapnn0fiub0  12793  hashnnn0genn0  13131  hashprb  13185  hash1snb  13207  hashgt12el  13210  hashgt12el2  13211  hash2prde  13252  hashge2el2dif  13262  hashge2el2difr  13263  dvdsaddre2b  15029  lcmf  15346  prmgaplem5  15759  cshwshashlem1  15802  acsfn  16320  symgfix2  17836  0ringnnzr  19269  mndifsplit  20442  symgmatr01lem  20459  xkopt  21458  umgrislfupgrlem  26017  lfgrwlkprop  26584  clwwlknclwwlkdifs  26873  frgr3vlem1  27137  frgrwopreg  27187  frgrregorufr  27189  frgrregord013  27253  jath  31609  hbimtg  31712  meran1  32410  imsym1  32417  ordcmp  32446  bj-curry  32542  bj-babygodel  32588  bj-ssbid2ALT  32646  bj-dvdemo1  32802  wl-jarli  33289  wl-lem-nexmo  33349  wl-ax11-lem2  33363  tsim2  33938  nexmo  34011  axc5c7toc7  34198  axc5c711toc7  34205  axc5c711to11  34206  ax12indi  34229  ifpim23g  37840  clsk1indlem3  38341  pm10.53  38565  pm11.63  38595  axc5c4c711  38602  axc5c4c711toc5  38603  axc5c4c711toc7  38605  axc5c4c711to11  38606  3ornot23  38715  notnotrALT  38735  hbimpg  38770  hbimpgVD  39140  notnotrALTVD  39151  climxrre  39982  liminf0  40025  prminf2  41500  nn0o1gt2ALTV  41605  nn0oALTV  41607  gbowge7  41651  nnsum3primesle9  41682  bgoldbtbndlem1  41693  lindslinindsimp1  42246