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  1389  3biant1d  1392  equsalh  1774  eueq3dc  2981  sbcel12g  3143  sbceqg  3144  sbcnel12g  3145  reldisj  3548  r19.3rm  3585  eldifpr  3700  eldiftp  3719  rabxp  4769  elrng  4927  iss  5065  eliniseg  5113  fcnvres  5528  dffv3g  5644  funimass4  5705  fndmdif  5761  fneqeql  5764  funimass3  5772  elrnrexdmb  5795  dff4im  5801  fconst4m  5882  elunirn  5917  riota1  6001  riota2df  6003  f1ocnvfv3  6017  eqfnov  6138  caoftrn  6277  suppimacnvfn  6424  suppssrst  6439  suppssrgst  6440  mpoxopovel  6450  rntpos  6466  ordgt0ge1  6646  iinerm  6819  erinxp  6821  qliftfun  6829  mapdm0  6875  elfi2  7214  fifo  7222  inl11  7307  ctssdccl  7353  isomnimap  7379  ismkvmap  7396  iswomnimap  7408  omniwomnimkv  7409  pr2nelem  7439  indpi  7605  genpdflem  7770  genpdisj  7786  genpassl  7787  genpassu  7788  ltnqpri  7857  ltpopr  7858  ltexprlemm  7863  ltexprlemdisj  7869  ltexprlemloc  7870  ltrennb  8117  letri3  8302  letr  8304  ltneg  8684  leneg  8687  reapltxor  8811  apsym  8828  suprnubex  9175  suprleubex  9176  elnnnn0  9487  zrevaddcl  9574  znnsub  9575  znn0sub  9589  prime  9623  eluz2  9805  eluz2b1  9879  nn01to3  9895  qrevaddcl  9922  xrletri3  10083  xrletr  10087  iccid  10204  elicopnf  10248  fzsplit2  10330  fzsn  10346  fzpr  10357  uzsplit  10372  fvinim0ffz  10533  lt2sqi  10935  le2sqi  10936  ccatlcan  11348  ccatrcan  11349  abs00ap  11685  iooinsup  11900  mertenslem2  12160  fprod2dlemstep  12246  gcddiv  12653  algcvgblem  12684  isprm3  12753  dvdsfi  12874  imasmnd2  13598  imasgrp2  13760  issubg  13823  resgrpisgrp  13845  eqgval  13873  imasrng  14033  ring1  14136  imasring  14141  crngunit  14189  lssle0  14451  lssats2  14493  zndvds  14728  znleval  14732  znleval2  14733  eltg2b  14848  discld  14930  opnssneib  14950  restbasg  14962  ssidcn  15004  cnptoprest2  15034  lmss  15040  txrest  15070  txlm  15073  imasnopn  15093  bldisj  15195  xmeter  15230  bl2ioo  15344  limcdifap  15456  issubgr  16181  bj-sseq  16493  nnti  16695  2omap  16698  pw1nct  16708