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  1386  3biant1d  1389  equsalh  1772  eueq3dc  2978  sbcel12g  3140  sbceqg  3141  sbcnel12g  3142  reldisj  3544  r19.3rm  3581  eldifpr  3694  eldiftp  3713  rabxp  4759  elrng  4917  iss  5055  eliniseg  5102  fcnvres  5515  dffv3g  5629  funimass4  5690  fndmdif  5746  fneqeql  5749  funimass3  5757  elrnrexdmb  5781  dff4im  5787  fconst4m  5867  elunirn  5900  riota1  5984  riota2df  5986  f1ocnvfv3  6000  eqfnov  6121  caoftrn  6261  mpoxopovel  6400  rntpos  6416  ordgt0ge1  6596  iinerm  6769  erinxp  6771  qliftfun  6779  mapdm0  6825  elfi2  7160  fifo  7168  inl11  7253  ctssdccl  7299  isomnimap  7325  ismkvmap  7342  iswomnimap  7354  omniwomnimkv  7355  pr2nelem  7385  indpi  7550  genpdflem  7715  genpdisj  7731  genpassl  7732  genpassu  7733  ltnqpri  7802  ltpopr  7803  ltexprlemm  7808  ltexprlemdisj  7814  ltexprlemloc  7815  ltrennb  8062  letri3  8248  letr  8250  ltneg  8630  leneg  8633  reapltxor  8757  apsym  8774  suprnubex  9121  suprleubex  9122  elnnnn0  9433  zrevaddcl  9518  znnsub  9519  znn0sub  9533  prime  9567  eluz2  9749  eluz2b1  9823  nn01to3  9839  qrevaddcl  9866  xrletri3  10027  xrletr  10031  iccid  10148  elicopnf  10192  fzsplit2  10273  fzsn  10289  fzpr  10300  uzsplit  10315  fvinim0ffz  10475  lt2sqi  10877  le2sqi  10878  ccatlcan  11286  ccatrcan  11287  abs00ap  11610  iooinsup  11825  mertenslem2  12084  fprod2dlemstep  12170  gcddiv  12577  algcvgblem  12608  isprm3  12677  dvdsfi  12798  imasmnd2  13522  imasgrp2  13684  issubg  13747  resgrpisgrp  13769  eqgval  13797  imasrng  13956  ring1  14059  imasring  14064  crngunit  14112  lssle0  14373  lssats2  14415  zndvds  14650  znleval  14654  znleval2  14655  eltg2b  14765  discld  14847  opnssneib  14867  restbasg  14879  ssidcn  14921  cnptoprest2  14951  lmss  14957  txrest  14987  txlm  14990  imasnopn  15010  bldisj  15112  xmeter  15147  bl2ioo  15261  limcdifap  15373  bj-sseq  16298  nnti  16501  2omap  16504  pw1nct  16514