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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitr4g  223  bibi2i  227  3bior1fd  1393  3biant1d  1396  equsalh  1778  eueq3dc  3000  sbcel12g  3162  sbceqg  3163  sbcnel12g  3164  reldisj  3576  r19.3rm  3616  eldifpr  3736  eldiftp  3755  rabxp  4812  elrng  4971  iss  5109  eliniseg  5157  fcnvres  5575  dffv3g  5691  funimass4  5753  fndmdif  5814  fneqeql  5817  funimass3  5825  elrnrexdmb  5848  dff4im  5854  fconst4m  5935  elunirn  5972  riota1  6058  riota2df  6060  f1ocnvfv3  6074  eqfnov  6195  caoftrn  6335  suppimacnvfn  6486  suppssrst  6501  suppssrgst  6502  mpoxopovel  6512  rntpos  6528  ordgt0ge1  6708  iinerm  6881  erinxp  6883  qliftfun  6891  mapdm0  6937  elfi2  7306  fifo  7314  2omap  7318  inl11  7405  ctssdccl  7451  isomnimap  7477  ismkvmap  7494  iswomnimap  7506  omniwomnimkv  7507  pr2nelem  7537  indpi  7709  genpdflem  7874  genpdisj  7890  genpassl  7891  genpassu  7892  ltnqpri  7961  ltpopr  7962  ltexprlemm  7967  ltexprlemdisj  7973  ltexprlemloc  7974  ltrennb  8221  letri3  8406  letr  8408  ltneg  8790  leneg  8793  reapltxor  8917  apsym  8934  suprnubex  9283  suprleubex  9284  elnnnn0  9606  fcdmnn0fsupp  9616  zrevaddcl  9695  znnsub  9696  znn0sub  9710  prime  9745  eluz2  9927  eluz2b1  10001  nn01to3  10017  qrevaddcl  10044  xrletri3  10206  xrletr  10210  iccid  10327  elicopnf  10371  fzsplit2  10455  fzsplit3  10458  fzsn  10472  fzpr  10484  uzsplit  10499  fvinim0ffz  10660  lt2sqi  11064  le2sqi  11065  sseqn  11279  hashf1lem1  11285  ccatlcan  11490  ccatrcan  11491  abs00ap  11828  iooinsup  12043  mertenslem2  12303  fprod2dlemstep  12389  gcddiv  12796  algcvgblem  12827  isprm3  12896  dvdsfi  13017  ballotfilemodife  13240  imasmnd2  13759  imasgrp2  13913  issubg  13976  resgrpisgrp  13998  eqgval  14026  imasrng  14255  ring1  14364  imasring  14369  crngunit  14418  lssle0  14709  lssats2  14751  zndvds  14984  znleval  14988  znleval2  14989  eltg2b  15155  discld  15237  opnssneib  15257  restbasg  15269  ssidcn  15311  cnptoprest2  15341  lmss  15347  txrest  15377  txlm  15380  imasnopn  15400  bldisj  15502  xmeter  15537  bl2ioo  15651  limcdifap  15763  issubgr  16498  bj-sseq  16820  nnti  17022  pw1nct  17033