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  1363  3biant1d  1366  equsalh  1748  eueq3dc  2946  sbcel12g  3107  sbceqg  3108  sbcnel12g  3109  reldisj  3511  r19.3rm  3548  eldifpr  3659  eldiftp  3678  rabxp  4710  elrng  4867  iss  5002  eliniseg  5049  fcnvres  5453  dffv3g  5566  funimass4  5623  fndmdif  5679  fneqeql  5682  funimass3  5690  elrnrexdmb  5714  dff4im  5720  fconst4m  5794  elunirn  5825  riota1  5908  riota2df  5910  f1ocnvfv3  5923  eqfnov  6042  caoftrn  6181  mpoxopovel  6317  rntpos  6333  ordgt0ge1  6511  iinerm  6684  erinxp  6686  qliftfun  6694  mapdm0  6740  elfi2  7056  fifo  7064  inl11  7149  ctssdccl  7195  isomnimap  7221  ismkvmap  7238  iswomnimap  7250  omniwomnimkv  7251  pr2nelem  7281  indpi  7437  genpdflem  7602  genpdisj  7618  genpassl  7619  genpassu  7620  ltnqpri  7689  ltpopr  7690  ltexprlemm  7695  ltexprlemdisj  7701  ltexprlemloc  7702  ltrennb  7949  letri3  8135  letr  8137  ltneg  8517  leneg  8520  reapltxor  8644  apsym  8661  suprnubex  9008  suprleubex  9009  elnnnn0  9320  zrevaddcl  9405  znnsub  9406  znn0sub  9420  prime  9454  eluz2  9636  eluz2b1  9704  nn01to3  9720  qrevaddcl  9747  xrletri3  9908  xrletr  9912  iccid  10029  elicopnf  10073  fzsplit2  10154  fzsn  10170  fzpr  10181  uzsplit  10196  fvinim0ffz  10351  lt2sqi  10753  le2sqi  10754  abs00ap  11292  iooinsup  11507  mertenslem2  11766  fprod2dlemstep  11852  gcddiv  12259  algcvgblem  12290  isprm3  12359  dvdsfi  12480  imasmnd2  13202  imasgrp2  13364  issubg  13427  resgrpisgrp  13449  eqgval  13477  imasrng  13636  ring1  13739  imasring  13744  crngunit  13791  lssle0  14052  lssats2  14094  zndvds  14329  znleval  14333  znleval2  14334  eltg2b  14444  discld  14526  opnssneib  14546  restbasg  14558  ssidcn  14600  cnptoprest2  14630  lmss  14636  txrest  14666  txlm  14669  imasnopn  14689  bldisj  14791  xmeter  14826  bl2ioo  14940  limcdifap  15052  bj-sseq  15592  nnti  15793  2omap  15796  pw1nct  15804