Theorem biimpi 149

Description: Infer an implication from a logical equivalence.

Hypothesis

Ref	Expression
biimp.1	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
biimpi	⊢ (φ → ψ)

Proof of Theorem biimpi

Step	Hyp	Ref	Expression
1		biimp.1	. 2 ⊢ (φ ↔ ψ)
2		bi1 146	. 2 ⊢ ((φ ↔ ψ) → (φ → ψ))
3	1, 2	ax-mp 7	1 ⊢ (φ → ψ)

Syntax hints:   → wi 3   ↔ wb 144

This theorem is referenced by:  bicomi 170  bitri 171  imbi2i 183  imbi1i 184  notbii 185  mpbi 187  sylib 196  sylbi 197  syl5ib 204  syl6ib 210  syl7ib 214  syl8ib 215  con1bii 218  pm1.2 243  pm1.4 245  pm2.62 246  orel1 249  pm1.5 257  pm2.32 260  pm3.1 312  pm3.26bi 320  pm3.27bi 324  pm3.3 346  pm3.22 440  sylanb 451  sylan2b 454  anbi2i 483  dfbi 518  pm5.16 670  nbn2 726  bimsc1 755  syl3an1b 868  syl3an2b 869  syl3an3b 870  nic-ax 969  stdpc5 1094  19.25 1120  sbbii 1211  exmoeu 1452  2mo 1487  eqeq1 1524  eleq2 1578  moeq 1966  ssel 2115  ss0 2356  prprc 2517  snsspr1 2534  eqsn 2539  elinti 2609  trel 2761  unipw 2836  moabex 2844  pocl 2922  wefrc 2970  unexg 3097  unisn2 3098  reuunixfr 3129  ordsson 3145  dflim3 3201  peano2 3238  elrel 3342  dmxp 3419  dmsnop 3577  coi2 3615  nfunv 3651  funun 3659  funcnv3 3663  funimass1 3677  funssxp 3745  dff1o2 3801  f1ocnv 3809  f1o00 3825  elrnopabg 3914  fsn2 3950  1stval 4142  2ndval 4143  1stdm 4169  tz7.49c 4261  oaabs 4392  elqsi 4431  qsexg 4434  0nelqs 4439  bren2 4530  pw2en 4587  ac6sfi 4591  canth2 4629  limenpsi 4652  php4 4663  unfilem1 4694  abfii4 4707  supmaxlem 4731  preleq 4748  inf3lem2 4759  r1tr 4800  rankr1 4820  rankr1b 4845  rankxplim2 4859  ac6lem 4900  kmlem6 4916  fodom 4944  unidom 4954  ficardom 4977  isinfcard 5037  iscard3 5038  alephval3 5053  dominf 5054  xrrebnd 5722  add20i 5756  posexi 6053  supxrun 6253  dfn2 6280  elnn0nn 6339  zindd 6386  icoshftf1oii 6536  cardfz 6671  seq1lem2 6675  expnlbnd 6853  nn0opthlem2 6866  crui 6938  recvalzi 7090  binomlem1 7269  binomlem2 7270  isumnul 7407  geoseri 7439  ivthlem6 7491  ivthlem7 7492  efaddlem5 7547  eirrlem5 7598  abspef01tlubi 7603  efgt1i 7611  reeff1olem1 7632  sin01bndlem2 7677  sin01bndlem3 7678  cos01bndlem2 7679  cos01bndlem3 7680  sin01gt0 7685  cos01gt0 7686  sin02gt0 7687  ruclem24 7745  ruclem27 7748  ruclem28 7749  infxpidmlem8 7771  isbasis3g 7825  subbas 7856  sn0top 7859  isopn2 7883  ntrval2 7896  innei 7946  cnpco 7979  dfms2 8009  metssba2 8020  grpidinvlem3 8263  gxsuc 8328  issubg 8358  subgres 8359  subgid 8362  subgabl 8365  vacnlem3 8584  vacnlem6 8587  sspval 8636  nmlno0lem 8708  blocni 8720  pythi 8766  pilem2 8939  pilem3 8940  efif 8993  efifolem7 9000  efif1lem3 9004  efif1lem4 9005  circgrp 9012  effoi 9017  normpythi 9285  omlsilem 9520  pjchi 9541  shmodsi 9638  chlubii 9671  nmlnop0iALT 10199  nmopun 10218  nmcopexlem1 10230  nmcfnexlem1 10259  cnlnssadj 10292  nmopcoi 10307  mdbr3 10505  mdbr4 10506  ssmd1 10519  dmdsl3 10523  mdslmd1lem2 10534  mdslmd4i 10541  mdexchi 10543  atssma 10587  atoml2i 10592  irredlem3 10601  mdsymlem1 10612  mdsymlem3 10614  dmdbr6ati 10632  dmdbr7ati 10633  cdjreui 10641  ghomgrpilem2 10671  difeqri2 10732  infi1 10735  fine 10736  ficli 10756  twpar2 10773  scprefat2 10784  fldleqt 10795  twsymr 10808  imfstnrelc 10810  infi 10854  tostos 10883  toplat 10884  exidu1 10902  on1el3 10962  mapdiscn 11014  cmphmp 11027  cnvhmphb 11032  cnvhmph 11033  hmphsyma 11034  hmeobc 11048  filintf 11081  fgsb 11082  efilcp 11083  efilcp2 11087  cnfilca 11088  rcfpfillem4 11092  sfvlim 11100  dtopcl 11107  dtt2 11110  stfincomp 11122  bsi2 11139  isalg 11175  algi 11181  dmrngcmp 11205  homib 11251  cmpmon 11270  idmon 11272  iepiclem 11278  idsubc 11305  idsubidsup 11311  idsubfun 11312  trer 11409  finminlem 11418  clsun 11465  opnregcld 11467  cldregopn 11468  subsubtop 11479  subcld 11480  cnsubsp 11483  cnsubsp2 11484  compsublem 11487  compsub 11488  compfipin0 11493  alexsublem4 11499  dfcon2 11501  connsub 11502  subtopmet 11506  reconnlem1 11507  reconn 11512  ivthALT 11515  2ndcsb 11537  2ndcctbss 11539  ssref 11553  topfneec 11562  fnessref 11564  refssfne 11565  locfindsc 11576  comppfsc 11578  topmtcl 11586  fnejoin1 11591  fnejoin2 11592  isnrm2 11613  opnfbas 11629  fbunfip 11631  supfil 11645  isufil2 11650  ufprim 11654  ufileu 11658  filufint 11659  ufinffr 11663  limfil 11675  hausfillim 11685  sfcls 11716  filclus 11717  fclsfnflim 11726  flimfnfcls 11727  gapmlem 11783  f1ocan2fv 11817  dif1en 11833  dif1card 11835  fimax 11837  indexf 11847  frinfm 11850  welb 11851  nninfnub 11882  subspopn 11900  subspcld 11901  subspabs 11903  mettrifi 11912  caushft 11916  cnres 11950  paste 11954  piececn 11955  txcn 11979  sstotbnd 11992  bndss 11998  totbndbnd 12000  heiborlem26 12036  heiborlem37 12047  heiborlem42 12052  bfp 12065  rrnmet 12072  rrndstprj 12073  rrndstprj2 12074  rrncms 12075  rrntotbnd 12078  phtpycom 12092  phtpycolem1 12093  phtpcer 12104

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 145

Copyright terms: Public domain