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  equsalh  1726  eueq3dc  2911  sbcel12g  3072  sbceqg  3073  sbcnel12g  3074  reldisj  3474  r19.3rm  3511  eldifpr  3619  eldiftp  3638  rabxp  4662  elrng  4817  iss  4952  eliniseg  4997  fcnvres  5398  dffv3g  5510  funimass4  5565  fndmdif  5620  fneqeql  5623  funimass3  5631  elrnrexdmb  5655  dff4im  5661  fconst4m  5735  elunirn  5764  riota1  5846  riota2df  5848  f1ocnvfv3  5861  eqfnov  5978  caoftrn  6105  mpoxopovel  6239  rntpos  6255  ordgt0ge1  6433  iinerm  6604  erinxp  6606  qliftfun  6614  mapdm0  6660  elfi2  6968  fifo  6976  inl11  7061  ctssdccl  7107  isomnimap  7132  ismkvmap  7149  iswomnimap  7161  omniwomnimkv  7162  pr2nelem  7187  indpi  7338  genpdflem  7503  genpdisj  7519  genpassl  7520  genpassu  7521  ltnqpri  7590  ltpopr  7591  ltexprlemm  7596  ltexprlemdisj  7602  ltexprlemloc  7603  ltrennb  7850  letri3  8034  letr  8036  ltneg  8415  leneg  8418  reapltxor  8542  apsym  8559  suprnubex  8906  suprleubex  8907  elnnnn0  9215  zrevaddcl  9299  znnsub  9300  znn0sub  9314  prime  9348  eluz2  9530  eluz2b1  9597  nn01to3  9613  qrevaddcl  9640  xrletri3  9800  xrletr  9804  iccid  9921  elicopnf  9965  fzsplit2  10045  fzsn  10061  fzpr  10072  uzsplit  10087  fvinim0ffz  10236  lt2sqi  10602  le2sqi  10603  abs00ap  11064  iooinsup  11278  mertenslem2  11537  fprod2dlemstep  11623  gcddiv  12012  algcvgblem  12041  isprm3  12110  phisum  12232  issubg  12964  resgrpisgrp  12986  eqgval  13013  ring1  13167  crngunit  13211  eltg2b  13425  discld  13507  opnssneib  13527  restbasg  13539  ssidcn  13581  cnptoprest2  13611  lmss  13617  txrest  13647  txlm  13650  imasnopn  13670  bldisj  13772  xmeter  13807  bl2ioo  13913  limcdifap  14002  bj-sseq  14404  nnti  14604  pw1nct  14612