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  881  falim  1559  rex0  4313  rmo0  4315  0ss  4353  rabsnifsb  4680  snsssn  4798  axnulALT  5250  dtrucor  5317  axc16b  5335  iresn0n0  6014  elfv2ex  6878  brfvopab  7417  el2mpocsbcl  8029  bropopvvv  8034  bropfvvvv  8036  tfrlem16  8326  omordi  8495  nnmordi  8561  omabs  8581  omsmolem  8587  0er  8676  pssnn  9097  fiint  9231  cantnfle  9584  r1sdom  9690  alephordi  9988  axdc3lem2  10365  canthp1  10569  elnnnn0b  12449  xltnegi  13135  xnn0xadd0  13166  xmulasslem2  13201  xrinf0  13258  elixx3g  13278  elfz2  13434  om2uzlti  13877  hashf1lem2  14383  hash3tpde  14420  relexpindlem  14990  sum0  15648  fsum2dlem  15697  prod0  15870  fprod2dlem  15907  nn0enne  16308  exprmfct  16635  prm23lt5  16746  4sqlem18  16894  vdwap0  16908  ram0  16954  prmlem1a  17038  prmlem2  17051  0catg  17615  dfgrp2e  18897  alexsub  23993  0met  24314  vitali  25574  plyeq0  26176  jensen  26959  ppiublem1  27173  ppiublem2  27174  lgsdir2lem3  27298  gausslemma2dlem0i  27335  2lgs  27378  2lgsoddprmlem3  27385  2sqnn  27410  2sqreultblem  27419  2sqreunnltblem  27422  rpvmasum  27497  sltsolem1  27647  nulsslt  27775  nulssgt  27776  vtxdg0v  29530  0enwwlksnge1  29920  rusgr0edg  30032  frgrreggt1  30451  topnfbey  30527  n0lpligALT  30542  sgn3da  32896  sgnnbi  32900  sgnpbi  32901  isarchi  33245  constrmon  33882  sibf0  34472  signstfvneq0  34710  bnj98  35004  bisym1  36594  unqsym1  36600  bj-godellob  36780  poimirlem30  37822  axc5sp1  39220  areaquad  43494  cantnfresb  43602  succlg  43606  oacl2g  43608  omabs2  43610  omcl2  43611  fiiuncl  45346  iblempty  46245  vonhoire  46952  fveqvfvv  47322  ralndv1  47387  ndmaovcl  47485  mod2addne  47646  prmdvdsfmtnof1lem2  47867  31prm  47879  lighneallem3  47889  fpprbasnn  48011  sbgoldbaltlem1  48061  bgoldbtbndlem1  48087  stgr0  48242  upwlkbprop  48420