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  890  pm5.75  965  xordidc  1419  19.17  1580  alexdc  1643  nf4dc  1694  abeq2d  2319  cbvralf  2731  cbvrexf  2732  cbvreu  2737  cbvrab  2771  ceqsralt  2801  ralab2  2941  rexab2  2943  euxfr2dc  2962  reu7  2972  reu8  2973  cbvralcsf  3160  cbvrexcsf  3161  cbvreucsf  3162  cbvrabcsf  3163  ralss  3263  rexss  3264  elif  3587  prssg  3796  2ralunsn  3845  eluniab  3868  elintab  3902  dfiun2g  3965  dfiin2g  3966  cbvopab1  4125  cbvmpt  4147  axsep2  4171  bnd2  4225  opeqsn  4305  reusv3  4515  tfisi  4643  opeliunxp  4738  eliunxp  4825  relop  4836  eldm2g  4883  reldm0  4905  relrn0  4949  restidsing  5024  xpmlem  5112  elxp5  5180  cnvpom  5234  cbviota  5246  iota1  5255  sniota  5271  fncnv  5349  fnres  5402  brprcneu  5582  fnopfvb  5633  fvelrnb  5639  fvelimab  5648  fvopab3g  5665  eqfnfv3  5692  eqfnfv2f  5694  fvreseq  5696  fnreseql  5703  rexsupp  5717  respreima  5721  rexrn  5730  ralrn  5731  f1ompt  5744  fsn  5765  fconstfvm  5815  fconst3m  5816  fconst4m  5817  foima2  5833  rexima  5836  ralima  5837  dff13  5850  foeqcnvco  5872  fliftfun  5878  isocnv  5893  isoini  5900  f1oiso  5908  cbvriota  5923  eusvobj2  5943  oprabid  5989  eloprabga  6045  resoprab  6054  eqfnov  6065  eqfnov2  6066  ov6g  6097  funimassov  6109  ovelimab  6110  caovord2  6132  uchoice  6236  releldm2  6284  dfoprab4  6291  xporderlem  6330  poxp  6331  f1od2  6334  mpoxopovel  6340  brtpos2  6350  brtpos0  6351  rntpos  6356  dftpos3  6361  tpostpos  6363  tpossym  6375  tposoprab  6379  tfrcllemres  6461  frecabcl  6498  frecsuclem  6505  erth2  6680  qliftfun  6717  erovlem  6727  ecopovsym  6731  ecopovsymg  6734  th3qlem1  6737  mapdm0  6763  elpmg  6764  elpm2g  6765  map0e  6786  dom2lem  6876  mapsnen  6917  xpdom2  6941  xpf1o  6956  mapen  6958  ssfilem  6987  diffitest  6999  ac6sfi  7010  ss1o0el1o  7025  isoti  7124  cnvti  7136  omp1eomlem  7211  ismkvnex  7272  nninfwlporlemd  7289  netap  7386  2omotaplemap  7389  ltexpi  7470  ordpipqqs  7507  ltexnqq  7541  enq0enq  7564  enq0sym  7565  enq0tr  7567  nqnq0pi  7571  genipv  7642  genprndl  7654  genprndu  7655  genpdisj  7656  genpassl  7657  genpassu  7658  addcomprg  7711  mulcomprg  7713  ltnqpr  7726  ltnqpri  7727  ltexprlemm  7733  ltexprlemdisj  7739  suplocexprlemmu  7851  suplocexprlemdisj  7853  ltsrprg  7880  mulgt0sr  7911  elreal2  7963  ltresr  7972  ltresr2  7973  axprecex  8013  axpre-ltadd  8019  axpre-mulgt0  8020  axpre-mulext  8021  axpre-suploclemres  8034  subcan2  8317  negcon1  8344  negcon2  8345  lt0neg1  8561  lt0neg2  8562  le0neg1  8563  le0neg2  8564  reapirr  8670  reapmul1  8688  reapneg  8690  remulext1  8692  apti  8715  negap0  8723  divmulap2  8769  reclt1  8989  recgt1  8990  suprleubex  9047  addltmul  9294  elznn0  9407  zapne  9467  zltlen  9471  nn0lt10b  9473  nn0lt2  9474  eluz1  9672  raluz  9719  rexuz  9721  qltlen  9781  cnref1o  9792  rpnegap  9828  ltxr  9917  xlt0neg1  9980  xlt0neg2  9981  xle0neg1  9982  xle0neg2  9983  elixx1  10039  elixx3g  10043  elioo2  10063  icc0r  10068  elicc4  10082  elioopnf  10109  elioomnf  10110  iooneg  10130  iccneg  10131  iccshftr  10136  iccshftl  10138  iccdil  10140  icccntr  10142  iccf1o  10146  elfz1  10155  0fz1  10187  fzpr  10219  fzdifsuc  10223  uzsplit  10234  elfzm1b  10240  elfzp12  10241  fznn0  10255  exfzdc  10391  zsupcllemstep  10394  flqeqceilz  10485  zmodid2  10519  expap0  10736  qsqeqor  10817  bernneq  10827  hasheqf1o  10952  hashfacen  11003  ccatrn  11088  pfxsuffeqwrdeq  11174  wrd2ind  11199  sqrtmsq2i  11521  maxclpr  11608  minmax  11616  xrmaxlesup  11645  xrnegiso  11648  xrnegcon1d  11650  xrminmax  11651  clim0  11671  climrecvg1n  11734  summodc  11769  fsumsplit  11793  mertenslem2  11922  prodmodc  11964  fprodsplitdc  11982  fprod2dlemstep  12008  dvdsval2  12176  odd2np1lem  12258  even2n  12260  divalgb  12311  divalgmod  12313  bitsval  12329  bitsmod  12342  gcddvds  12359  bezoutlemmain  12394  nnwofdc  12434  isprm3  12515  prmind2  12517  dvdsprime  12519  coprm  12541  prmdvdsexp  12545  sqrt2irr  12559  sqpweven  12572  2sqpwodd  12573  pythagtriplem2  12664  pythagtrip  12681  pceu  12693  pc11  12729  elrest  13153  grpsubeq0  13493  grpsubadd  13495  issubg3  13603  isnsg  13613  eqger  13635  eqglact  13636  eqgid  13637  srgfcl  13810  dvdsrtr  13938  dvdsr02  13942  isunitd  13943  isrhm  13995  isrim0  13998  subsubrng2  14052  subsubrg2  14083  issubrg3  14084  opprdomnbg  14111  2idlelb  14342  mplelbascoe  14529  istopon  14560  isbasis2g  14592  isbasis3g  14593  tgss2  14626  bastop1  14630  iscld  14650  ntreq0  14679  restsn  14727  restopn2  14730  lmbr  14760  cnptoprest2  14787  txbas  14805  eltx  14806  txlm  14826  ishmeo  14851  hmeoimaf1o  14861  ispsmet  14870  ismet  14891  isxmet  14892  ismet2  14901  metn0  14925  elblps  14937  elbl  14938  bdbl  15050  qtopbasss  15068  elcncf  15120  ellimc3apf  15207  elply  15281  sincosq1sgn  15373  sincosq2sgn  15374  cos11  15400  logrpap0b  15423  lgsdir2lem4  15583  gausslemma2dlem0i  15609  lgsquadlem2  15630  m1lgs  15637  2lgsoddprmlem3  15663  2sqlem6  15672  2sqlem9  15676  2sqlem10  15677  2omap  16071  pw1map  16073  subctctexmid  16078  iooref1o  16114  iswomni0  16131