Theorem con3i 114

Description: A contraposition inference.

Hypothesis

Ref	Expression
con3.a	|- (ph -> ps)

Assertion

Ref	Expression
con3i	|- (-. ps -> -. ph)

Proof of Theorem con3i

Step	Hyp	Ref	Expression
1		notnot2 100	. . 3 |- (-. -. ph -> ph)
2		con3.a	. . 3 |- (ph -> ps)
3	1, 2	syl 12	. 2 |- (-. -. ph -> ps)
4	3	con1i 112	1 |- (-. ps -> -. ph)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.5 115  pm2.51 116  pm2.52 117  mto 121  nsyl 131  notbii 204  pm2.45 299  pm2.46 300  orim12i 363  pm5.14 728  pm5.21ni 742  con3th 843  equidqe 1314  equidq 1315  ax4 1318  ax67 1367  ax67to6 1368  ax467to6 1372  19.29OLD 1422  sbn 1601  ax11indalem 1759  a12lem2 1768  euor2 1839  moexex 1841  necon3aiOLD 2044  necon3biOLD 2046  necon1bi 2048  sbc2or 2481  difrab 2868  noel 2879  ifor 3008  snex 3492  mosubopt 3551  eldifpw 3854  nlimsucg 3923  nlimsucgOLD 3924  tfindsg 3944  findsg 3980  vtoclibr 4035  soirri 4314  nfvres 4705  fvopab4ndm 4747  fvopabn 4749  oprprc1 4908  ndmoprass 4981  ndmoprdistr 4982  curry1val 5077  curry2val 5080  canth 5112  eceqopreq 5372  fiprc 5492  ensdomtr 5534  sdomirr 5535  sdomen2 5545  pwuninel 5550  2pwuninel 5551  en2lp 5707  isfinite 5741  nnsdom 5742  rankxplim3 5825  rankxpsuc 5826  ac6n 5919  ac9s 5926  kmlem2 5928  alephnbtwn 6016  alephnbtwn2 6017  alephval2 6050  dominf 6052  cdainf 6087  nd3 6092  axrepnd 6098  nlt1pi 6185  lt1nnn 7130  zeo 7411  uzssz 7599  sumsqne0i 7879  nnesqi 7912  climcl 8238  clmi1i 8346  ruclem28 8806  grpidval 9342  issubg 9425  avril1 10142  nonbooli 11231  chpssati 11935  bnj1144 12941  ressn0 13829  distel 13870  predpoirr 13908  predfrirr 13909  rb-ax2 14220  rb-ax4 14222  nandsym1 14246  evpexun 14322  fiiu 14344  neiopne 14354  isfinite1b 14434  hmeogrp 14892  fgsb 14921  fgsb2 14925  cnfilca 14927  rcfpfillem2 14929  difxp 15690  frinfm 15758  heiborlem39 15993  pm10.251 16306  ax4567to6 16362  en3lpVD 16669

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

Copyright terms: Public domain