HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem impbi 157
Description: Infer an equivalence from an implication and its converse.
Hypotheses
Ref Expression
impbi.1 |- (ph -> ps)
impbi.2 |- (ps -> ph)
Assertion
Ref Expression
impbi |- (ph <-> ps)
Proof of Theorem impbi
StepHypRef Expression
1 impbi.1 . 2 |- (ph -> ps)
2 impbi.2 . 2 |- (ps -> ph)
3 bi3 150 . 2 |- ((ph -> ps) -> ((ps -> ph) -> (ph <-> ps)))
41, 2, 3mp2 43 1 |- (ph <-> ps)
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146
This theorem is referenced by:  bii 158  bi2.04 160  pm4.13 161  pm4.8 162  pm4.81 163  pm4.1 164  bi2.03 165  bi2.15 166  pm5.4 167  imdi 168  pm5.41 169  pm4.2 170  bicomi 172  bitr 173  imbi2i 185  imbi1i 186  negbii 187  a1bi 197  con1bii 220  dfor2 229  oridm 243  anclb 329  ancrb 330  pm4.45im 332  pm4.44 345  pm5.63 346  impexp 347  jaob 422  pm4.43 431  anidm 432  ancom 435  imdistan 442  pm5.3 446  pm5.61 447  abai 478  anbi2i 479  anabs1 491  anabs7 493  orabs 579  pm5.74 581  ordi 594  pm4.71 633  pm4.72 639  oibabs 652  pm5.18 658  mt2bi 711  2th 716  bianfi 735  pm4.82 737  orbidi 741  consensus 765  19.3 1027  alcom 1028  19.9 1032  excom 1042  19.21 1052  19.23 1059  19.26 1063  equcom 1125  equsal 1147  sbbii 1170  sbf 1182  sb6x 1184  equs45f 1196  sb6f 1197  dfsb2 1220  sbn 1226  sbim 1229  sb5rf 1254  sb6rf 1255  sb8 1256  sb9 1259  equvin 1270  mo 1386  eu2 1389  mo2 1393  exmoeu 1406  2mo 1440  2eu6 1447  ralcom3 1769  rabab 1813  ceqsex 1825  gencbvex2 1830  euxfr2 1916  reu3 1921  reu6 1922  sspss 2135  ssin 2222  unineq 2245  uneqin 2246  difrab 2263  un00 2296  vss 2297  ralf0 2349  elpr2 2415  snidb 2424  disjsn 2431  pwpw0 2460  prss 2462  sssn 2464  sspr 2466  tpss 2467  preq12b 2474  preqsn 2477  iununi 2606  intex 2719  intnex 2720  iin0 2730  sspwb 2745  sspwuni 2748  opth 2777  opprc1b 2786  opprc3 2787  opthwiener 2796  ssopab2 2811  pwssun 2816  pwundif 2817  unexb 2864  ralxfr 2889  reuxfr2 2893  uniexb 2897  iunpw 2904  dfwe2 2925  elon2 2949  ordeleqon 2980  onintrab 3003  unon 3078  onuninsuc 3098  ordzsl 3106  dflim3 3108  ralxp 3208  opthprc 3211  relop 3265  issetid 3269  xpid11 3324  iss 3381  cotr 3420  cnvsym 3421  asymref2 3424  asymref2OLD 3426  xpnz 3452  ssrnres 3467  dfrel2 3471  unixp0 3504  dffun7 3526  fn0 3591  fnopabg 3601  fnf 3614  funssxp 3623  f00 3642  dffo2 3660  f1o2 3678  ffoss 3696  f1o00 3699  fo00 3700  fv3 3718  fnopabfv 3743  dff4 3801  dff2 3802  dffo4 3805  dffo5 3806  exfo 3807  fopab2 3808  rnssopab 3810  ffnfv 3813  fsn 3819  fsn2 3821  fconstfv 3834  abianfp 3947  ersymb 4257  mapval2 4319  map0 4328  mapsn 4329  bren2 4370  en0 4404  en1 4407  pw2en 4426  canth2 4464  mapxpen 4475  xpmapenlem5 4480  0sdom1dom 4504  unfilem1 4524  fiint 4534  pwfi 4545  sucprcreg 4572  opthreg 4576  suc11reg 4577  infeq5 4593  elom3 4603  isfinite 4606  rankr1 4646  rankonid 4667  rankeq0 4668  rankr1id 4669  rankuni 4670  rankxplim3 4686  scott0 4689  karden 4698  aceq3 4705  aceq4 4706  aceq5lem3 4709  aceq5 4712  aceq7 4715  ac9s 4736  kmlem2 4738  kmlem13 4749  fodomb 4772  brdom3 4773  brdom5 4774  brdom4 4775  brdom7disj 4776  brdom6disj 4777  oncard 4801  cardlim 4823  alephgeom 4854  iscard3 4860  cdainf 4909  reclem1pr 5128  mappsrpr 5190  map2psrpr 5192  supsrlem1 5197  supsrlem2 5198  addcan 5323  le2tri3 5563  ltadd2 5564  mulcan 5659  mul0or 5663  rec11i 5733  eqneg 5760  ltmul1i 5777  nnsub 5903  dfn2 6059  elnnz 6092  elnn0z 6094  elnnz1 6102  elnn0nn 6118  elnnnn0b 6120  elnnnn0c 6121  nneo 6144  om2uzran 6237  elioo4g 6318  eluzfz2b 6422  elfz2nn0t 6427  sumsqne0 6565  nnesq 6592  nn0opth 6596  sqr0 6602  cru 6667  crne0 6670  rereb 6715  negreb 6730  abs00 6777  absgt0 6778  abslt 6810  absle 6811  absltOLD 6812  absleOLD 6813  cau5 6856  cvg1 6858  cvg2 6859  cvg3 6860  cvganz 6861  climshft 7041  efltb 7348  dscmet 7856  xplm 7909  iscms2 7928  issubg 8053  nmlno0lem 8385  isblo3i 8392  blocni 8396  cosh111lem2 8630  circgrp 8660  hvsubeq0 8851  hvaddcan 8853  bcseq 8907  hlimreu 9031  hlimeu 9032  norm1ex 9043  hhsssh 9059  dfch2 9164  pjoc1 9179  pjch 9180  shlub 9261  shslub 9273  shs00 9288  chsscon3 9299  chlejb1 9314  chj00 9325  shjshsel 9331  h1de2ctlem 9394  spanunsn 9419  cmcm 9452  cmbr3 9460  cmbr4 9461  pjrn 9564  pj11 9573  hosubeq0 9669  dmadjrnb 9747  nmlnop0ALT 9835  lnopeq0 9847  elunop2t 9853  lnopcon 9878  lncnopbd 9881  lnfncon 9905  adjbdlnb 9932  adjbd1o 9933  rnbra 9953  pjss1co 10002  pjss2co 10003  pjnormss 10007  pjssdif2 10013  pjssdif1 10014  pjhmopidm 10020  pjinvar 10029  pjin2 10031  pjc 10038  pjcmmul1 10039  pjcmmul2 10040  strb 10095  hstrb 10103  mdsl1 10156  atom1d 10188  chrelat2 10200  cvbr3 10202  cvexch 10204  sumdmd 10254  dmdbr5at 10255  dmdbr6at 10256  cdj3 10273  and4as 10332  and4com 10333  fiv 10374  dtopcl 10459
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