Theorem biimp 151

Description: Infer an implication from a logical equivalence.

Hypothesis

Ref	Expression
biimp.1	|- (ph <-> ps)

Assertion

Ref	Expression
biimp	|- (ph -> ps)

Proof of Theorem biimp

Step	Hyp	Ref	Expression
1		biimp.1	. 2 |- (ph <-> ps)
2		bi1 148	. 2 |- ((ph <-> ps) -> (ph -> ps))
3	1, 2	ax-mp 7	1 |- (ph -> ps)

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  bicomi 172  bitr 173  imbi2i 185  imbi1i 186  negbii 187  mpbi 189  sylib 198  sylbi 199  syl5ib 206  syl6ib 212  syl7ib 216  syl8ib 217  con1bii 220  pm1.2 245  pm1.4 247  pm2.62 248  orel1 251  pm1.5 259  pm2.32 262  pm3.1 314  pm3.26bi 322  pm3.27bi 326  pm3.3 348  pm3.22 438  sylanb 449  sylan2b 452  anbi2i 480  pm5.16 666  nbn2 720  bimsc1 749  syl3an1b 861  syl3an2b 862  syl3an3b 863  nicodraw 951  mpgbi 986  stdpc5 1057  19.25 1083  sbbii 1174  exmoeu 1413  2mo 1447  eqeq1 1480  eleq2 1534  moeq 1918  ssel 2061  ss0 2301  prprc 2452  snsspr 2468  eqsn 2472  elinti 2539  trel 2684  moabex 2763  pocl 2841  unexg 2871  unisn2 2872  reuunixfr 2903  wefrc 2940  ordsson 2988  dflim3 3115  peano2 3147  elrel 3250  dmsnop 3325  dmxp 3329  coi2 3508  nfunv 3543  funun 3551  funcnv3 3555  funimass1 3569  funssxp 3635  f1o2 3690  f1ocnv 3698  f1o00 3711  elrnopabg 3797  fsn2 3833  tz7.49c 3957  1stval 4078  2ndval 4079  1st2val 4092  2nd2val 4093  1stdm 4106  oaabs 4249  elqsi 4288  qsexg 4291  0nelqs 4295  bren2 4383  pw2en 4439  canth2 4477  limenpsi 4498  php4 4509  unfilem1 4537  abfii4 4551  supmaxlem 4575  preleq 4590  inf3lem2 4601  r1tr 4641  rankr1 4661  rankr1b 4686  rankxplim2 4700  ac6lem 4741  kmlem6 4757  fodom 4785  unidom 4795  isinfcard 4874  iscard3 4875  alephval3 4890  dominf 4891  xrrebndt 5555  add20 5590  posex 5870  supxrun 6046  dfn2 6073  elnn0nn 6132  seq1lem2 6265  icoshftf1oi 6360  expnlbndt 6605  nn0opthlem2 6615  nn0opthlem2OLD 6616  cru 6688  recvalz 6852  binomlem1 7034  binomlem2 7035  isumnul 7174  geoser 7205  ivthlem6 7257  ivthlem7 7258  ivthlem4OLD 7264  ivthlem6OLD 7266  ivthlem7OLD 7267  ivthOLD 7269  ivth2OLD 7270  efaddlem5 7320  efsubt 7349  eirrlem5 7370  abspef01tlub 7372  efgt1 7380  reeff1olem1 7400  reeff1olem1OLD 7402  sin01bndlem2 7446  sin01bndlem3 7447  cos01bndlem2 7448  cos01bndlem3 7449  sin01gt0 7454  cos01gt0 7455  sin02gt0 7456  ruclem24 7512  ruclem27 7515  ruclem28 7516  infxpidmlem8 7538  isbasis3g 7592  subbas 7623  sn0top 7626  isopn2 7652  ntrval2 7665  innei 7715  cnpco 7748  dfms2 7778  metssba2 7789  grpidinvlem3 8033  issubg 8101  subgres 8102  subgid 8105  subgabl 8108  sspval 8368  nmlno0lem 8438  blocni 8449  pythi 8494  pilem2 8655  pilem3 8656  efif 8700  efifolem4 8704  efifolem7 8707  efif1lem3 8711  efif1lem4 8712  circcltOLD 8720  circgrp 8724  effoi 8729  normpyth 8993  omlsilem 9232  pjch 9253  shmods 9350  chlubi 9383  nmlnop0ALT 9911  nmopunt 9930  nmcopexlem1 9942  nmcfnexlem1 9971  cnlnssadj 10004  nmopco 10019  mdbr3 10215  mdbr4 10216  ssmd1 10229  dmdsl3t 10233  mdslmd1lem2 10244  mdslmd4 10251  mdexch 10253  atssmat 10296  atoml2 10301  irredlem3 10310  mdsymlem1 10321  mdsymlem3 10323  dmdbr6at 10341  dmdbr7at 10342  cdjreu 10350  ghomgrpilem2 10377  gelcomplOLD 10410  faimpex 10432  difeqri2 10437  infi1 10440  fine 10441  ficli 10461  mapdiscn 10492  cmphmp 10502  cnvhmphb 10507  cnvhmph 10508  hmphsyma 10509  filintf 10537  fgsb 10538  efilcp 10539  infi 10542  efilcp2 10544  cnfilca 10545  rcfpfillem4 10549  sfvlim 10557  dtopcl 10566  dtt2 10569  isalg 10604  algi 10611  homib 10675  cmpmon 10692  idmon 10695

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain