Theorem bitr4di 198

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

Hypotheses

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

Assertion

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

Proof of Theorem bitr4di

Step	Hyp	Ref	Expression
1		bitr4di.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		bitr4di.2	. . 3 |- ( th <-> ch )
3	2	bicomi 132	. 2 |- ( ch <-> th )
4	1, 3	bitrdi 196	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:  3bitr4g  223  bibi2i  227  3bior1fd  1388  3biant1d  1391  equsalh  1774  eueq3dc  2980  sbcel12g  3142  sbceqg  3143  sbcnel12g  3144  reldisj  3546  r19.3rm  3583  eldifpr  3696  eldiftp  3715  rabxp  4763  elrng  4921  iss  5059  eliniseg  5106  fcnvres  5520  dffv3g  5635  funimass4  5696  fndmdif  5752  fneqeql  5755  funimass3  5763  elrnrexdmb  5787  dff4im  5793  fconst4m  5874  elunirn  5907  riota1  5991  riota2df  5993  f1ocnvfv3  6007  eqfnov  6128  caoftrn  6268  mpoxopovel  6407  rntpos  6423  ordgt0ge1  6603  iinerm  6776  erinxp  6778  qliftfun  6786  mapdm0  6832  elfi2  7171  fifo  7179  inl11  7264  ctssdccl  7310  isomnimap  7336  ismkvmap  7353  iswomnimap  7365  omniwomnimkv  7366  pr2nelem  7396  indpi  7562  genpdflem  7727  genpdisj  7743  genpassl  7744  genpassu  7745  ltnqpri  7814  ltpopr  7815  ltexprlemm  7820  ltexprlemdisj  7826  ltexprlemloc  7827  ltrennb  8074  letri3  8260  letr  8262  ltneg  8642  leneg  8645  reapltxor  8769  apsym  8786  suprnubex  9133  suprleubex  9134  elnnnn0  9445  zrevaddcl  9530  znnsub  9531  znn0sub  9545  prime  9579  eluz2  9761  eluz2b1  9835  nn01to3  9851  qrevaddcl  9878  xrletri3  10039  xrletr  10043  iccid  10160  elicopnf  10204  fzsplit2  10285  fzsn  10301  fzpr  10312  uzsplit  10327  fvinim0ffz  10488  lt2sqi  10890  le2sqi  10891  ccatlcan  11303  ccatrcan  11304  abs00ap  11640  iooinsup  11855  mertenslem2  12115  fprod2dlemstep  12201  gcddiv  12608  algcvgblem  12639  isprm3  12708  dvdsfi  12829  imasmnd2  13553  imasgrp2  13715  issubg  13778  resgrpisgrp  13800  eqgval  13828  imasrng  13988  ring1  14091  imasring  14096  crngunit  14144  lssle0  14405  lssats2  14447  zndvds  14682  znleval  14686  znleval2  14687  eltg2b  14797  discld  14879  opnssneib  14899  restbasg  14911  ssidcn  14953  cnptoprest2  14983  lmss  14989  txrest  15019  txlm  15022  imasnopn  15042  bldisj  15144  xmeter  15179  bl2ioo  15293  limcdifap  15405  issubgr  16127  bj-sseq  16439  nnti  16642  2omap  16645  pw1nct  16655