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  880  falim  1554  rex0  4366  rmo0  4368  0ss  4406  r19.2zb  4502  rabsnifsb  4727  snsssn  4846  axnulALT  5310  dtrucor  5377  axc16b  5395  iresn0n0  6074  elfv2ex  6953  brfvopab  7490  el2mpocsbcl  8109  bropopvvv  8114  bropfvvvv  8116  tfrlem16  8432  omordi  8603  nnmordi  8668  omabs  8688  omsmolem  8694  0er  8782  pssnn  9207  fiint  9364  fiintOLD  9365  cantnfle  9709  r1sdom  9812  alephordi  10112  axdc3lem2  10489  canthp1  10692  elnnnn0b  12568  xltnegi  13255  xnn0xadd0  13286  xmulasslem2  13321  xrinf0  13377  elixx3g  13397  elfz2  13551  om2uzlti  13988  hashf1lem2  14492  hash3tpde  14529  relexpindlem  15099  sum0  15754  fsum2dlem  15803  prod0  15976  fprod2dlem  16013  nn0enne  16411  exprmfct  16738  prm23lt5  16848  4sqlem18  16996  vdwap0  17010  ram0  17056  prmlem1a  17141  prmlem2  17154  0catg  17733  dfgrp2e  18994  alexsub  24069  0met  24392  vitali  25662  plyeq0  26265  jensen  27047  ppiublem1  27261  ppiublem2  27262  lgsdir2lem3  27386  gausslemma2dlem0i  27423  2lgs  27466  2lgsoddprmlem3  27473  2sqnn  27498  2sqreultblem  27507  2sqreunnltblem  27510  rpvmasum  27585  sltsolem1  27735  nulsslt  27857  nulssgt  27858  vtxdg0v  29506  0enwwlksnge1  29894  rusgr0edg  30003  frgrreggt1  30422  topnfbey  30498  n0lpligALT  30513  isarchi  33172  constrmon  33749  sibf0  34316  sgn3da  34523  sgnnbi  34527  sgnpbi  34528  signstfvneq0  34566  bnj98  34860  bisym1  36402  unqsym1  36408  bj-godellob  36588  poimirlem30  37637  axc5sp1  38905  areaquad  43205  cantnfresb  43314  succlg  43318  oacl2g  43320  omabs2  43322  omcl2  43323  fiiuncl  45005  iblempty  45921  vonhoire  46628  fveqvfvv  46990  ralndv1  47055  ndmaovcl  47153  prmdvdsfmtnof1lem2  47510  31prm  47522  lighneallem3  47532  fpprbasnn  47654  sbgoldbaltlem1  47704  bgoldbtbndlem1  47730  uspgrimprop  47811  stgr0  47863  upwlkbprop  47982