Theorem pm2.21i 115

Description: A contradiction implies anything. Inference associated with pm2.21 119. Its associated inference is pm2.24ii 116. (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 112	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  116  notnotri  125  pm2.21dd  185  pm3.2ni  895  falim  1489  nfnthOLD  1727  rex0  3894  0ss  3924  r19.2zb  4013  ral0  4028  rabsnifsb  4201  snsssn  4312  int0OLD  4426  axnulALT  4715  axc16b  4784  dtrucor  4827  elfv2ex  6139  brfvopab  6598  el2mpt2csbcl  7137  bropopvvv  7142  bropfvvvv  7144  tfrlem16  7376  omordi  7533  nnmordi  7598  omabs  7614  omsmolem  7620  0er  7667  0erOLD  7668  pssnn  8063  fiint  8122  cantnfle  8451  r1sdom  8520  alephordi  8780  axdc3lem2  9156  canthp1  9355  elnnnn0b  11214  xltnegi  11921  xnn0xadd0  11949  xmulasslem2  11984  xrinf0  12039  elixx3g  12059  elfz2  12204  om2uzlti  12611  hashf1lem2  13097  sum0  14299  fsum2dlem  14343  prod0  14512  fprod2dlem  14549  zeneo  14901  nn0enne  14932  exprmfct  15254  prm23lt5  15357  4sqlem18  15504  vdwap0  15518  ram0  15564  prmlem1a  15651  prmlem2  15665  xpsfrnel2  16048  0catg  16171  dfgrp2e  17271  alexsub  21659  0met  21981  vitali  23188  plyeq0  23771  jensen  24515  ppiublem1  24727  ppiublem2  24728  lgsdir2lem3  24852  gausslemma2dlem0i  24889  2lgs  24932  2lgsoddprmlem3  24939  rpvmasum  25015  usgraedgprv  25905  4cycl4dv  26195  clwwlknprop  26300  2wlkonot3v  26402  2spthonot3v  26403  frgrareggt1  26643  topnfbey  26717  isarchi  29067  sibf0  29723  sgn3da  29930  sgnnbi  29934  sgnpbi  29935  signstfvneq0  29975  bnj98  30191  sltsolem1  31067  bisym1  31588  unqsym1  31594  amosym1  31595  subsym1  31596  bj-godellob  31763  bj-axc16b  31986  bj-dtrucor  31988  poimirlem30  32609  axc5sp1  33226  areaquad  36821  fiiuncl  38259  iblempty  38857  vonhoire  39563  fveqvfvv  39853  ndmaovcl  39932  prmdvdsfmtnof1lem2  40035  31prm  40050  lighneallem3  40062  sgoldbaltlem1  40201  bgoldbtbndlem1  40221  vtxdg0v  40688  wlkbProp  40817  0enwwlksnge1  41060  wwlks2onv  41158  rusgr0edg  41176  av-frgrareggt1  41547