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  1388  3biant1d  1391  equsalh  1774  eueq3dc  2980  sbcel12g  3142  sbceqg  3143  sbcnel12g  3144  reldisj  3546  r19.3rm  3583  eldifpr  3696  eldiftp  3715  rabxp  4763  elrng  4921  iss  5059  eliniseg  5106  fcnvres  5520  dffv3g  5635  funimass4  5696  fndmdif  5752  fneqeql  5755  funimass3  5763  elrnrexdmb  5787  dff4im  5793  fconst4m  5873  elunirn  5906  riota1  5990  riota2df  5992  f1ocnvfv3  6006  eqfnov  6127  caoftrn  6267  mpoxopovel  6406  rntpos  6422  ordgt0ge1  6602  iinerm  6775  erinxp  6777  qliftfun  6785  mapdm0  6831  elfi2  7170  fifo  7178  inl11  7263  ctssdccl  7309  isomnimap  7335  ismkvmap  7352  iswomnimap  7364  omniwomnimkv  7365  pr2nelem  7395  indpi  7561  genpdflem  7726  genpdisj  7742  genpassl  7743  genpassu  7744  ltnqpri  7813  ltpopr  7814  ltexprlemm  7819  ltexprlemdisj  7825  ltexprlemloc  7826  ltrennb  8073  letri3  8259  letr  8261  ltneg  8641  leneg  8644  reapltxor  8768  apsym  8785  suprnubex  9132  suprleubex  9133  elnnnn0  9444  zrevaddcl  9529  znnsub  9530  znn0sub  9544  prime  9578  eluz2  9760  eluz2b1  9834  nn01to3  9850  qrevaddcl  9877  xrletri3  10038  xrletr  10042  iccid  10159  elicopnf  10203  fzsplit2  10284  fzsn  10300  fzpr  10311  uzsplit  10326  fvinim0ffz  10486  lt2sqi  10888  le2sqi  10889  ccatlcan  11298  ccatrcan  11299  abs00ap  11622  iooinsup  11837  mertenslem2  12096  fprod2dlemstep  12182  gcddiv  12589  algcvgblem  12620  isprm3  12689  dvdsfi  12810  imasmnd2  13534  imasgrp2  13696  issubg  13759  resgrpisgrp  13781  eqgval  13809  imasrng  13968  ring1  14071  imasring  14076  crngunit  14124  lssle0  14385  lssats2  14427  zndvds  14662  znleval  14666  znleval2  14667  eltg2b  14777  discld  14859  opnssneib  14879  restbasg  14891  ssidcn  14933  cnptoprest2  14963  lmss  14969  txrest  14999  txlm  15002  imasnopn  15022  bldisj  15124  xmeter  15159  bl2ioo  15273  limcdifap  15385  issubgr  16107  bj-sseq  16388  nnti  16591  2omap  16594  pw1nct  16604