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  195  pm3.2ni  879  falim  1554  rex0  4383  rmo0  4385  0ss  4423  r19.2zb  4519  rabsnifsb  4747  snsssn  4866  axnulALT  5322  dtrucor  5389  axc16b  5407  iresn0n0  6083  elfv2ex  6966  brfvopab  7507  el2mpocsbcl  8126  bropopvvv  8131  bropfvvvv  8133  tfrlem16  8449  omordi  8622  nnmordi  8687  omabs  8707  omsmolem  8713  0er  8801  pssnn  9234  fiint  9394  fiintOLD  9395  cantnfle  9740  r1sdom  9843  alephordi  10143  axdc3lem2  10520  canthp1  10723  elnnnn0b  12597  xltnegi  13278  xnn0xadd0  13309  xmulasslem2  13344  xrinf0  13400  elixx3g  13420  elfz2  13574  om2uzlti  14001  hashf1lem2  14505  hash3tpde  14542  relexpindlem  15112  sum0  15769  fsum2dlem  15818  prod0  15991  fprod2dlem  16028  nn0enne  16425  exprmfct  16751  prm23lt5  16861  4sqlem18  17009  vdwap0  17023  ram0  17069  prmlem1a  17154  prmlem2  17167  0catg  17746  dfgrp2e  19003  alexsub  24074  0met  24397  vitali  25667  plyeq0  26270  jensen  27050  ppiublem1  27264  ppiublem2  27265  lgsdir2lem3  27389  gausslemma2dlem0i  27426  2lgs  27469  2lgsoddprmlem3  27476  2sqnn  27501  2sqreultblem  27510  2sqreunnltblem  27513  rpvmasum  27588  sltsolem1  27738  nulsslt  27860  nulssgt  27861  vtxdg0v  29509  0enwwlksnge1  29897  rusgr0edg  30006  frgrreggt1  30425  topnfbey  30501  n0lpligALT  30516  isarchi  33162  constrmon  33734  sibf0  34299  sgn3da  34506  sgnnbi  34510  sgnpbi  34511  signstfvneq0  34549  bnj98  34843  bisym1  36385  unqsym1  36391  bj-godellob  36571  poimirlem30  37610  axc5sp1  38879  areaquad  43177  cantnfresb  43286  succlg  43290  oacl2g  43292  omabs2  43294  omcl2  43295  fiiuncl  44967  iblempty  45886  vonhoire  46593  fveqvfvv  46955  ralndv1  47020  ndmaovcl  47118  prmdvdsfmtnof1lem2  47459  31prm  47471  lighneallem3  47481  fpprbasnn  47603  sbgoldbaltlem1  47653  bgoldbtbndlem1  47679  uspgrimprop  47757  upwlkbprop  47861