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  11079  le2sqi  11080  sseqn  11295  hashf1lem1  11301  ccatlcan  11506  ccatrcan  11507  abs00ap  11844  iooinsup  12062  mertenslem2  12322  fprod2dlemstep  12408  gcddiv  12815  algcvgblem  12846  isprm3  12915  dvdsfi  13040  ballotfilemodife  13292  imasmnd2  13812  imasgrp2  13966  issubg  14029  resgrpisgrp  14051  eqgval  14079  imasrng  14339  ring1  14448  imasring  14453  crngunit  14502  lssle0  14793  lssats2  14835  zndvds  15068  znleval  15072  znleval2  15073  eltg2b  15246  discld  15328  opnssneib  15348  restbasg  15360  ssidcn  15402  cnptoprest2  15432  lmss  15438  txrest  15468  txlm  15471  imasnopn  15491  bldisj  15593  xmeter  15628  bl2ioo  15742  limcdifap  15854  bposlem6  16277  issubgr  16664  bj-sseq  16986  nnti  17188  pw1nct  17199