Theorem pm2.21i 119

Description: A contradiction implies anything. Inference associated with pm2.21 123. Its associated inference is pm2.24ii 120. (Contributed by NM, 16-Sep-1993.)

Hypothesis

Ref	Expression
pm2.21i.1	⊢ ¬ 𝜑

Assertion

Ref	Expression
pm2.21i	⊢ (𝜑 → 𝜓)

Proof of Theorem pm2.21i

Step	Hyp	Ref	Expression
1		pm2.21i.1	. . 3 ⊢ ¬ 𝜑
2	1	a1i 11	. 2 ⊢ (¬ 𝜓 → ¬ 𝜑)
3	2	con4i 114	1 ⊢ (𝜑 → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  pm2.24ii  120  notnotri  131  notnotriALT  132  pm2.21dd  194  pm3.2ni  878  falim  1550  rex0  4361  rmo0  4363  0ss  4400  r19.2zb  4499  ral0OLD  4520  rabsnifsb  4731  snsssn  4847  axnulALT  5308  dtrucor  5375  axc16b  5393  iresn0n0  6062  elfv2ex  6948  brfvopab  7483  el2mpocsbcl  8096  bropopvvv  8101  bropfvvvv  8103  tfrlem16  8420  omordi  8593  nnmordi  8658  omabs  8678  omsmolem  8684  0er  8768  pssnn  9199  pssnnOLD  9296  fiint  9356  cantnfle  9702  r1sdom  9805  alephordi  10105  axdc3lem2  10482  canthp1  10685  elnnnn0b  12554  xltnegi  13235  xnn0xadd0  13266  xmulasslem2  13301  xrinf0  13357  elixx3g  13377  elfz2  13531  om2uzlti  13955  hashf1lem2  14457  relexpindlem  15050  sum0  15707  fsum2dlem  15756  prod0  15927  fprod2dlem  15964  nn0enne  16361  exprmfct  16682  prm23lt5  16790  4sqlem18  16938  vdwap0  16952  ram0  16998  prmlem1a  17083  prmlem2  17096  0catg  17675  dfgrp2e  18927  alexsub  23969  0met  24292  vitali  25562  plyeq0  26165  jensen  26941  ppiublem1  27155  ppiublem2  27156  lgsdir2lem3  27280  gausslemma2dlem0i  27317  2lgs  27360  2lgsoddprmlem3  27367  2sqnn  27392  2sqreultblem  27401  2sqreunnltblem  27404  rpvmasum  27479  sltsolem1  27628  nulsslt  27750  nulssgt  27751  vtxdg0v  29307  0enwwlksnge1  29695  rusgr0edg  29804  frgrreggt1  30223  topnfbey  30299  n0lpligALT  30314  isarchi  32911  sibf0  33987  sgn3da  34194  sgnnbi  34198  sgnpbi  34199  signstfvneq0  34237  bnj98  34531  bisym1  35936  unqsym1  35942  bj-godellob  36115  poimirlem30  37156  axc5sp1  38427  areaquad  42675  cantnfresb  42784  succlg  42788  oacl2g  42790  omabs2  42792  omcl2  42793  fiiuncl  44460  iblempty  45382  vonhoire  46089  fveqvfvv  46451  ralndv1  46514  ndmaovcl  46612  prmdvdsfmtnof1lem2  46954  31prm  46966  lighneallem3  46976  fpprbasnn  47098  sbgoldbaltlem1  47148  bgoldbtbndlem1  47174  uspgrimprop  47249  upwlkbprop  47278