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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-3 8

This theorem is used by:  pm2.24ii  121  notnotri  132  notnotriALT  133  pm2.21dd  198  pm3.2ni  894  falim  1587  rex0  4311  rmo0  4313  0ss  4353  rabsnifsb  4686  snsssn  4804  axnulALT  5265  dtrucor  5340  axc16b  5358  iresn0n0  6054  elfv2ex  6925  brfvopab  7474  el2mpocsbcl  8086  bropopvvv  8091  bropfvvvv  8093  tfrlem16  8386  omordi  8557  nnmordi  8623  omabs  8643  omsmolem  8649  0er  8739  pssnn  9167  fiint  9300  cantnfle  9654  r1sdom  9760  alephordi  10081  axdc3lem2  10457  canthp1  10667  elnnnn0b  12576  xltnegi  13272  xnn0xadd0  13303  xmulasslem2  13338  xrinf0  13395  elixx3g  13415  elfz2  13572  om2uzlti  14018  hashf1lem2  14525  hash3tpde  14562  relexpindlem  15140  sgn3da  15178  sgnnbi  15181  sgnpbi  15182  sum0  15811  fsum2dlem  15860  prod0  16036  fprod2dlem  16073  nn0enne  16473  exprmfct  16801  prm23lt5  16912  4sqlem18  17060  vdwap0  17074  ram0  17120  prmlem1a  17204  prmlem2  17218  0catg  17782  dfgrp2e  19093  alexsub  24277  0met  24598  vitali  25847  plyeq0  26444  jensen  27233  ppiublem1  27446  ppiublem2  27447  lgsdir2lem3  27571  gausslemma2dlem0i  27608  2lgs  27651  2lgsoddprmlem3  27658  2sqnn  27683  2sqreultblem  27692  2sqreunnltblem  27695  rpvmasum  27770  ltssolem1  27919  nulslts  28048  nulsgts  28049  vtxdg0v  29941  0enwwlksnge1  30340  rusgr0edg  30452  frgrreggt1  30881  topnfbey  30957  n0lpligALT  30973  isarchi  33630  constrmon  34262  sibf0  34853  signstfvneq0  35088  bnj98  35384  axnulALT2  35598  bisym1  37046  unqsym1  37052  bj-godellob  37314  poimirlem30  38407  axc5sp1  39804  areaquad  44065  cantnfresb  44173  succlg  44177  oacl2g  44179  omabs2  44181  omcl2  44182  fiiuncl  45907  iblempty  46801  vonhoire  47508  fveqvfvv  47936  ralndv1  48001  ndmaovcl  48099  mod2addne  48266  prmdvdsfmtnof1lem2  48496  31prm  48508  lighneallem3  48518  nprmdvdsfacm1lem2  48532  fpprbasnn  48653  sbgoldbaltlem1  48703  bgoldbtbndlem1  48729  stgr0  48884  upwlkbprop  49062  prmringnzring  49260