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  7319  inl11  7406  ctssdccl  7452  isomnimap  7478  ismkvmap  7495  iswomnimap  7507  omniwomnimkv  7508  pr2nelem  7538  indpi  7710  genpdflem  7875  genpdisj  7891  genpassl  7892  genpassu  7893  ltnqpri  7962  ltpopr  7963  ltexprlemm  7968  ltexprlemdisj  7974  ltexprlemloc  7975  ltrennb  8222  letri3  8407  letr  8409  ltneg  8792  leneg  8795  reapltxor  8920  apsym  8937  suprnubex  9286  suprleubex  9287  elnnnn0  9611  fcdmnn0fsupp  9621  zrevaddcl  9700  znnsub  9701  znn0sub  9715  prime  9750  eluz2  9937  eluz2b1  10011  nn01to3  10027  qrevaddcl  10054  xrletri3  10217  xrletr  10221  iccid  10338  elicopnf  10382  fzsplit2  10466  fzsplit3  10469  fzsn  10483  fzpr  10495  uzsplit  10510  fvinim0ffz  10671  lt2sqi  11078  le2sqi  11079  sseqn  11294  hashf1lem1  11300  ccatlcan  11505  ccatrcan  11506  abs00ap  11843  iooinsup  12061  mertenslem2  12321  fprod2dlemstep  12407  gcddiv  12814  algcvgblem  12845  isprm3  12914  dvdsfi  13039  ballotfilemodife  13291  imasmnd2  13810  imasgrp2  13964  issubg  14027  resgrpisgrp  14049  eqgval  14077  imasrng  14306  ring1  14415  imasring  14420  crngunit  14469  lssle0  14760  lssats2  14802  zndvds  15035  znleval  15039  znleval2  15040  eltg2b  15207  discld  15289  opnssneib  15309  restbasg  15321  ssidcn  15363  cnptoprest2  15393  lmss  15399  txrest  15429  txlm  15432  imasnopn  15452  bldisj  15554  xmeter  15589  bl2ioo  15703  limcdifap  15815  issubgr  16620  bj-sseq  16942  nnti  17144  pw1nct  17155