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  1389  3biant1d  1392  equsalh  1774  eueq3dc  2994  sbcel12g  3156  sbceqg  3157  sbcnel12g  3158  reldisj  3564  r19.3rm  3602  eldifpr  3721  eldiftp  3740  rabxp  4792  elrng  4951  iss  5089  eliniseg  5137  fcnvres  5555  dffv3g  5671  funimass4  5732  fndmdif  5788  fneqeql  5791  funimass3  5799  elrnrexdmb  5822  dff4im  5828  fconst4m  5909  elunirn  5945  riota1  6031  riota2df  6033  f1ocnvfv3  6047  eqfnov  6168  caoftrn  6308  suppimacnvfn  6459  suppssrst  6474  suppssrgst  6475  mpoxopovel  6485  rntpos  6501  ordgt0ge1  6681  iinerm  6854  erinxp  6856  qliftfun  6864  mapdm0  6910  elfi2  7272  fifo  7280  2omap  7282  inl11  7369  ctssdccl  7415  isomnimap  7441  ismkvmap  7458  iswomnimap  7470  omniwomnimkv  7471  pr2nelem  7501  indpi  7673  genpdflem  7838  genpdisj  7854  genpassl  7855  genpassu  7856  ltnqpri  7925  ltpopr  7926  ltexprlemm  7931  ltexprlemdisj  7937  ltexprlemloc  7938  ltrennb  8185  letri3  8370  letr  8372  ltneg  8753  leneg  8756  reapltxor  8880  apsym  8897  suprnubex  9244  suprleubex  9245  elnnnn0  9556  fcdmnn0fsupp  9566  zrevaddcl  9645  znnsub  9646  znn0sub  9660  prime  9695  eluz2  9877  eluz2b1  9951  nn01to3  9967  qrevaddcl  9994  xrletri3  10156  xrletr  10160  iccid  10277  elicopnf  10321  fzsplit2  10404  fzsplit3  10407  fzsn  10421  fzpr  10433  uzsplit  10448  fvinim0ffz  10609  lt2sqi  11013  le2sqi  11014  sseqn  11228  ccatlcan  11435  ccatrcan  11436  abs00ap  11772  iooinsup  11987  mertenslem2  12247  fprod2dlemstep  12333  gcddiv  12740  algcvgblem  12771  isprm3  12840  dvdsfi  12961  ballotfilemodife  13184  imasmnd2  13707  imasgrp2  13863  issubg  13926  resgrpisgrp  13948  eqgval  13976  imasrng  14195  ring1  14302  imasring  14307  crngunit  14356  lssle0  14646  lssats2  14688  zndvds  14923  znleval  14927  znleval2  14928  eltg2b  15045  discld  15127  opnssneib  15147  restbasg  15159  ssidcn  15201  cnptoprest2  15231  lmss  15237  txrest  15267  txlm  15270  imasnopn  15290  bldisj  15392  xmeter  15427  bl2ioo  15541  limcdifap  15653  issubgr  16378  bj-sseq  16690  nnti  16892  pw1nct  16903