Theorem pm2.21i 116

Description: A contradiction implies anything. Inference associated with pm2.21 120. Its associated inference is pm2.24ii 117. (Contributed by NM, 16-Sep-1993.)

Hypothesis

Ref	Expression
pm2.21i.1	|- -. ph

Assertion

Ref	Expression
pm2.21i	|- ( ph -> ps )

Proof of Theorem pm2.21i

Step	Hyp	Ref	Expression
1		pm2.21i.1	. . 3 |- -. ph
2	1	a1i 11	. 2 |- ( -. ps -> -. ph )
3	2	con4i 113	1 |- ( ph -> ps )

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  117  notnotri  126  pm2.21dd  186  pm3.2ni  899  falim  1498  nfnthOLD  1736  rex0  3938  0ss  3972  r19.2zb  4061  ral0  4076  rabsnifsb  4257  snsssn  4372  int0OLD  4491  axnulALT  4787  axc16b  4858  dtrucor  4900  elfv2ex  6229  brfvopab  6700  el2mpt2csbcl  7250  bropopvvv  7255  bropfvvvv  7257  tfrlem16  7489  omordi  7646  nnmordi  7711  omabs  7727  omsmolem  7733  0er  7780  0erOLD  7781  pssnn  8178  fiint  8237  cantnfle  8568  r1sdom  8637  alephordi  8897  axdc3lem2  9273  canthp1  9476  elnnnn0b  11337  xltnegi  12047  xnn0xadd0  12077  xmulasslem2  12112  xrinf0  12168  elixx3g  12188  elfz2  12333  om2uzlti  12749  hashf1lem2  13240  sum0  14452  fsum2dlem  14501  prod0  14673  fprod2dlem  14710  nn0enne  15094  exprmfct  15416  prm23lt5  15519  4sqlem18  15666  vdwap0  15680  ram0  15726  prmlem1a  15813  prmlem2  15827  xpsfrnel2  16225  0catg  16348  dfgrp2e  17448  alexsub  21849  0met  22171  vitali  23382  plyeq0  23967  jensen  24715  ppiublem1  24927  ppiublem2  24928  lgsdir2lem3  25052  gausslemma2dlem0i  25089  2lgs  25132  2lgsoddprmlem3  25139  rpvmasum  25215  vtxdg0v  26369  0enwwlksnge1  26749  wwlks2onv  26847  rusgr0edg  26868  frgrreggt1  27251  topnfbey  27325  n0lpligALT  27336  isarchi  29736  sibf0  30396  sgn3da  30603  sgnnbi  30607  sgnpbi  30608  signstfvneq0  30649  bnj98  30937  sltsolem1  31826  bisym1  32418  unqsym1  32424  amosym1  32425  subsym1  32426  bj-godellob  32590  bj-axc16b  32798  bj-dtrucor  32800  poimirlem30  33439  opabf  34131  axc5sp1  34208  areaquad  37802  fiiuncl  39234  iblempty  40181  vonhoire  40886  fveqvfvv  41204  ndmaovcl  41283  prmdvdsfmtnof1lem2  41497  31prm  41512  lighneallem3  41524  sbgoldbaltlem1  41667  bgoldbtbndlem1  41693  upwlkbprop  41719