Theorem bitrdi 196

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitrdi.1	|- ( ph -> ( ps <-> ch ) )
bitrdi.2	|- ( ch <-> th )

Assertion

Ref	Expression
bitrdi	|- ( ph -> ( ps <-> th ) )

Proof of Theorem bitrdi

Step	Hyp	Ref	Expression
1		bitrdi.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		bitrdi.2	. . 3 |- ( ch <-> th )
3	2	a1i 9	. 2 |- ( ph -> ( ch <-> th ) )
4	1, 3	bitrd 188	1 |- ( ph -> ( ps <-> th ) )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bitr2di  197  bitr4di  198  3bitr3g  222  bibi2i  227  ibibr  246  biancomd  271  imanst  900  pm5.75  975  xordidc  1448  19.17  1609  alexdc  1672  nf4dc  1722  abeq2d  2351  eqabrd  2378  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvrab  2819  ceqsralt  2849  ralab2  2990  rexab2  2992  euxfr2dc  3011  reu7  3021  reu8  3022  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  ralss  3314  rexss  3315  elif  3649  prssg  3867  2ralunsn  3919  eluniab  3942  elintab  3976  dfiun2g  4039  dfiin2g  4040  cbvopab1  4199  cbvmpt  4221  axsepg  4245  bnd2  4305  opeqsn  4388  reusv3  4601  tfisi  4729  opeliunxp  4825  eliunxp  4914  relop  4925  eldm2g  4972  reldm0  4994  relrn0  5039  restidsing  5114  xpmlem  5203  elxp5  5271  cnvpom  5325  cbviota  5337  iota1  5347  sniota  5363  fncnv  5442  fnres  5495  brprcneu  5683  fnopfvb  5736  fvelrnb  5744  fvelimab  5753  fvopab3g  5772  eqfnfv3  5799  eqfnfv2f  5801  fvreseq  5803  fnreseql  5810  respreima  5827  rexrn  5836  ralrn  5837  f1ompt  5850  fsn  5871  fconstfvm  5924  fconst3m  5925  fconst4m  5926  foima2  5947  rexima  5950  ralima  5951  dff13  5964  foeqcnvco  5986  fliftfun  5992  isocnv  6007  isoini  6014  f1oiso  6022  cbvriota  6040  riotaeqimp  6053  eusvobj2  6061  oprabid  6107  eloprabga  6165  resoprab  6174  eqfnov  6185  eqfnov2  6186  ov6g  6217  funimassov  6229  ovelimab  6230  caovord2  6252  uchoice  6361  releldm2  6409  dfoprab4  6416  xporderlem  6457  poxp  6458  f1od2  6461  elsuppfng  6472  elsuppfn  6473  rexsupp  6483  mpoxopovel  6502  brtpos2  6512  brtpos0  6513  rntpos  6518  dftpos3  6523  tpostpos  6525  tpossym  6537  tposoprab  6541  tfrcllemres  6623  frecabcl  6660  frecsuclem  6667  erth2  6844  qliftfun  6881  erovlem  6891  ecopovsym  6895  ecopovsymg  6898  th3qlem1  6901  mapdm0  6927  elpmg  6928  elpm2g  6929  map0e  6957  dom2lem  7048  mapsnend  7089  mapsnen  7090  xpdom2  7119  xpf1o  7134  mapen  7136  ssfilem  7167  ssfilemd  7169  diffitest  7181  ac6sfi  7192  eqsndc  7200  ss1o0el1o  7210  2omap  7308  isoti  7337  cnvti  7349  omp1eomlem  7424  ismkvnex  7485  nninfwlporlemd  7502  en2prde  7529  netap  7610  2omotaplemap  7613  ltexpi  7694  ordpipqqs  7731  ltexnqq  7765  enq0enq  7788  enq0sym  7789  enq0tr  7791  nqnq0pi  7795  genipv  7866  genprndl  7878  genprndu  7879  genpdisj  7880  genpassl  7881  genpassu  7882  addcomprg  7935  mulcomprg  7937  ltnqpr  7950  ltnqpri  7951  ltexprlemm  7957  ltexprlemdisj  7963  suplocexprlemmu  8075  suplocexprlemdisj  8077  ltsrprg  8104  mulgt0sr  8135  elreal2  8187  ltresr  8196  ltresr2  8197  axprecex  8237  axpre-ltadd  8243  axpre-mulgt0  8244  axpre-mulext  8245  axpre-suploclemres  8258  subcan2  8541  negcon1  8568  negcon2  8569  lt0neg1  8786  lt0neg2  8787  le0neg1  8788  le0neg2  8789  reapirr  8895  reapmul1  8913  reapneg  8915  remulext1  8917  apti  8940  negap0  8948  divmulap2  8996  reclt1  9216  recgt1  9217  suprleubex  9274  addltmul  9521  elznn0  9638  zapne  9698  zltlen  9703  nn0lt10b  9705  nn0lt2  9706  eluz1  9904  raluz  9957  rexuz  9959  qltlen  10019  cnref1o  10030  rpnegap  10066  ltxr  10156  xlt0neg1  10219  xlt0neg2  10220  xle0neg1  10221  xle0neg2  10222  elixx1  10278  elixx3g  10282  elioo2  10302  icc0r  10307  elicc4  10321  elioopnf  10348  elioomnf  10349  iooneg  10369  iccneg  10370  iccshftr  10375  iccshftl  10377  iccdil  10379  icccntr  10381  iccf1o  10386  elfz1  10395  0fz1  10428  fzpr  10462  fzdifsuc  10466  uzsplit  10477  elfzm1b  10483  elfzp12  10484  fznn0  10498  exfzdc  10637  zsupcllemstep  10640  flqeqceilz  10733  zmodid2  10767  expap0  10984  qsqeqor  11065  bernneq  11076  hasheqf1o  11202  ssenneg  11258  hashfibclem  11260  hashfacen  11262  hashf1  11265  ccatrn  11355  pfxsuffeqwrdeq  11448  wrd2ind  11473  sqrtmsq2i  11879  maxclpr  11966  minmax  11974  xrmaxlesup  12003  xrnegiso  12006  xrnegcon1d  12008  xrminmax  12009  clim0  12029  climrecvg1n  12092  summodc  12128  fsumsplit  12152  mertenslem2  12281  prodmodc  12323  fprodsplitdc  12341  fprod2dlemstep  12367  dvdsval2  12535  odd2np1lem  12617  even2n  12619  divalgb  12670  divalgmod  12672  bitsval  12688  bitsmod  12701  gcddvds  12718  bezoutlemmain  12753  nnwofdc  12793  isprm3  12874  prmind2  12876  dvdsprime  12878  coprm  12900  prmdvdsexp  12904  sqrt2irr  12918  sqpweven  12931  2sqpwodd  12932  pythagtriplem2  13023  pythagtrip  13040  pceu  13052  pc11  13088  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemodife  13218  elrest  13577  grpsubeq0  13868  grpsubadd  13870  issubg3  13972  isnsg  13982  eqger  14004  eqglact  14005  eqgid  14006  srgfcl  14251  dvdsrtr  14381  dvdsr02  14385  isunitd  14386  isrhm  14438  isrim0  14441  subsubrng2  14496  subsubrg2  14527  issubrg3  14528  opprdomnbg  14556  2idlelb  14814  mplelbascoe  15006  istopon  15037  isbasis2g  15069  isbasis3g  15070  tgss2  15103  bastop1  15107  iscld  15127  ntreq0  15156  restsn  15204  restopn2  15207  lmbr  15237  cnptoprest2  15264  txbas  15282  eltx  15283  txlm  15303  ishmeo  15328  hmeoimaf1o  15338  ispsmet  15347  ismet  15368  isxmet  15369  ismet2  15378  metn0  15402  elblps  15414  elbl  15415  bdbl  15527  qtopbasss  15545  elcncf  15597  ellimc3apf  15684  elply  15758  sincosq1sgn  15850  sincosq2sgn  15851  cos11  15877  logrpap0b  15900  lgsdir2lem4  16064  gausslemma2dlem0i  16090  lgsquadlem2  16111  m1lgs  16118  2lgsoddprmlem3  16144  2sqlem6  16153  2sqlem9  16157  2sqlem10  16158  vtxdfifiun  16452  wlkl1loop  16513  wlkv0  16524  wlklenvclwlk  16528  upgr2wlkdc  16532  isclwwlk  16549  isclwwlkng  16561  isclwwlknx  16571  clwwlkn2  16576  eupth2lem2dc  16614  eupth2lem3lem6fi  16626  pw1map  16939  subctctexmid  16944  iooref1o  16988  iswomni0  17006