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  1386  3biant1d  1389  equsalh  1772  eueq3dc  2977  sbcel12g  3139  sbceqg  3140  sbcnel12g  3141  reldisj  3543  r19.3rm  3580  eldifpr  3693  eldiftp  3712  rabxp  4755  elrng  4912  iss  5050  eliniseg  5097  fcnvres  5508  dffv3g  5622  funimass4  5683  fndmdif  5739  fneqeql  5742  funimass3  5750  elrnrexdmb  5774  dff4im  5780  fconst4m  5858  elunirn  5889  riota1  5973  riota2df  5975  f1ocnvfv3  5989  eqfnov  6110  caoftrn  6249  mpoxopovel  6385  rntpos  6401  ordgt0ge1  6579  iinerm  6752  erinxp  6754  qliftfun  6762  mapdm0  6808  elfi2  7135  fifo  7143  inl11  7228  ctssdccl  7274  isomnimap  7300  ismkvmap  7317  iswomnimap  7329  omniwomnimkv  7330  pr2nelem  7360  indpi  7525  genpdflem  7690  genpdisj  7706  genpassl  7707  genpassu  7708  ltnqpri  7777  ltpopr  7778  ltexprlemm  7783  ltexprlemdisj  7789  ltexprlemloc  7790  ltrennb  8037  letri3  8223  letr  8225  ltneg  8605  leneg  8608  reapltxor  8732  apsym  8749  suprnubex  9096  suprleubex  9097  elnnnn0  9408  zrevaddcl  9493  znnsub  9494  znn0sub  9508  prime  9542  eluz2  9724  eluz2b1  9792  nn01to3  9808  qrevaddcl  9835  xrletri3  9996  xrletr  10000  iccid  10117  elicopnf  10161  fzsplit2  10242  fzsn  10258  fzpr  10269  uzsplit  10284  fvinim0ffz  10442  lt2sqi  10844  le2sqi  10845  ccatlcan  11245  ccatrcan  11246  abs00ap  11568  iooinsup  11783  mertenslem2  12042  fprod2dlemstep  12128  gcddiv  12535  algcvgblem  12566  isprm3  12635  dvdsfi  12756  imasmnd2  13480  imasgrp2  13642  issubg  13705  resgrpisgrp  13727  eqgval  13755  imasrng  13914  ring1  14017  imasring  14022  crngunit  14069  lssle0  14330  lssats2  14372  zndvds  14607  znleval  14611  znleval2  14612  eltg2b  14722  discld  14804  opnssneib  14824  restbasg  14836  ssidcn  14878  cnptoprest2  14908  lmss  14914  txrest  14944  txlm  14947  imasnopn  14967  bldisj  15069  xmeter  15104  bl2ioo  15218  limcdifap  15330  bj-sseq  16114  nnti  16315  2omap  16318  pw1nct  16328