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  1740  eueq3dc  2938  sbcel12g  3099  sbceqg  3100  sbcnel12g  3101  reldisj  3503  r19.3rm  3540  eldifpr  3650  eldiftp  3669  rabxp  4701  elrng  4858  iss  4993  eliniseg  5040  fcnvres  5444  dffv3g  5557  funimass4  5614  fndmdif  5670  fneqeql  5673  funimass3  5681  elrnrexdmb  5705  dff4im  5711  fconst4m  5785  elunirn  5816  riota1  5899  riota2df  5901  f1ocnvfv3  5914  eqfnov  6033  caoftrn  6172  mpoxopovel  6308  rntpos  6324  ordgt0ge1  6502  iinerm  6675  erinxp  6677  qliftfun  6685  mapdm0  6731  elfi2  7047  fifo  7055  inl11  7140  ctssdccl  7186  isomnimap  7212  ismkvmap  7229  iswomnimap  7241  omniwomnimkv  7242  pr2nelem  7270  indpi  7426  genpdflem  7591  genpdisj  7607  genpassl  7608  genpassu  7609  ltnqpri  7678  ltpopr  7679  ltexprlemm  7684  ltexprlemdisj  7690  ltexprlemloc  7691  ltrennb  7938  letri3  8124  letr  8126  ltneg  8506  leneg  8509  reapltxor  8633  apsym  8650  suprnubex  8997  suprleubex  8998  elnnnn0  9309  zrevaddcl  9393  znnsub  9394  znn0sub  9408  prime  9442  eluz2  9624  eluz2b1  9692  nn01to3  9708  qrevaddcl  9735  xrletri3  9896  xrletr  9900  iccid  10017  elicopnf  10061  fzsplit2  10142  fzsn  10158  fzpr  10169  uzsplit  10184  fvinim0ffz  10334  lt2sqi  10736  le2sqi  10737  abs00ap  11244  iooinsup  11459  mertenslem2  11718  fprod2dlemstep  11804  gcddiv  12211  algcvgblem  12242  isprm3  12311  dvdsfi  12432  imasmnd2  13154  imasgrp2  13316  issubg  13379  resgrpisgrp  13401  eqgval  13429  imasrng  13588  ring1  13691  imasring  13696  crngunit  13743  lssle0  14004  lssats2  14046  zndvds  14281  znleval  14285  znleval2  14286  eltg2b  14374  discld  14456  opnssneib  14476  restbasg  14488  ssidcn  14530  cnptoprest2  14560  lmss  14566  txrest  14596  txlm  14599  imasnopn  14619  bldisj  14721  xmeter  14756  bl2ioo  14870  limcdifap  14982  bj-sseq  15522  nnti  15723  2omap  15726  pw1nct  15734