Theorem pm2.21i 120

Description: A contradiction implies anything. Inference associated with pm2.21 124. Its associated inference is pm2.24ii 121. (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 115	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  121  notnotri  132  notnotriALT  133  pm2.21dd  198  pm3.2ni  893  falim  1580  rex0  4316  rmo0  4318  0ss  4357  rabsnifsb  4684  snsssn  4802  axnulALT  5259  dtrucor  5333  axc16b  5351  iresn0n0  6047  elfv2ex  6914  brfvopab  7457  el2mpocsbcl  8068  bropopvvv  8073  bropfvvvv  8075  tfrlem16  8368  omordi  8539  nnmordi  8605  omabs  8625  omsmolem  8631  0er  8721  pssnn  9141  fiint  9274  cantnfle  9628  r1sdom  9734  alephordi  10046  axdc3lem2  10423  canthp1  10627  elnnnn0b  12539  xltnegi  13233  xnn0xadd0  13264  xmulasslem2  13299  xrinf0  13356  elixx3g  13376  elfz2  13533  om2uzlti  13977  hashf1lem2  14483  hash3tpde  14520  relexpindlem  15090  sgn3da  15128  sgnnbi  15131  sgnpbi  15132  sum0  15762  fsum2dlem  15811  prod0  15987  fprod2dlem  16024  nn0enne  16425  exprmfct  16753  prm23lt5  16864  4sqlem18  17012  vdwap0  17026  ram0  17072  prmlem1a  17156  prmlem2  17170  0catg  17734  dfgrp2e  19020  alexsub  24163  0met  24484  vitali  25733  plyeq0  26329  jensen  27111  ppiublem1  27324  ppiublem2  27325  lgsdir2lem3  27449  gausslemma2dlem0i  27486  2lgs  27529  2lgsoddprmlem3  27536  2sqnn  27561  2sqreultblem  27570  2sqreunnltblem  27573  rpvmasum  27648  ltssolem1  27797  nulslts  27926  nulsgts  27927  vtxdg0v  29732  0enwwlksnge1  30122  rusgr0edg  30234  frgrreggt1  30653  topnfbey  30729  n0lpligALT  30745  isarchi  33415  constrmon  34051  sibf0  34641  signstfvneq0  34876  bnj98  35172  axnulALT2  35387  bisym1  36792  unqsym1  36798  bj-godellob  37060  poimirlem30  38161  axc5sp1  39559  areaquad  43805  cantnfresb  43913  succlg  43917  oacl2g  43919  omabs2  43921  omcl2  43922  fiiuncl  45643  iblempty  46537  vonhoire  47244  fveqvfvv  47632  ralndv1  47697  ndmaovcl  47795  mod2addne  47962  prmdvdsfmtnof1lem2  48192  31prm  48204  lighneallem3  48214  nprmdvdsfacm1lem2  48228  fpprbasnn  48349  sbgoldbaltlem1  48399  bgoldbtbndlem1  48425  stgr0  48580  upwlkbprop  48758  prmringnzring  48957