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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitr4g  223  bibi2i  227  3bior1fd  1393  3biant1d  1396  equsalh  1778  eueq3dc  3000  sbcel12g  3162  sbceqg  3163  sbcnel12g  3164  reldisj  3576  r19.3rm  3616  eldifpr  3736  eldiftp  3755  rabxp  4812  elrng  4971  iss  5109  eliniseg  5157  fcnvres  5575  dffv3g  5691  funimass4  5753  fndmdif  5814  fneqeql  5817  funimass3  5825  elrnrexdmb  5848  dff4im  5854  fconst4m  5935  elunirn  5972  riota1  6058  riota2df  6060  f1ocnvfv3  6074  eqfnov  6195  caoftrn  6335  suppimacnvfn  6486  suppssrst  6501  suppssrgst  6502  mpoxopovel  6512  rntpos  6528  ordgt0ge1  6708  iinerm  6881  erinxp  6883  qliftfun  6891  mapdm0  6937  elfi2  7306  fifo  7314  2omap  7318  inl11  7405  ctssdccl  7451  isomnimap  7477  ismkvmap  7494  iswomnimap  7506  omniwomnimkv  7507  pr2nelem  7537  indpi  7709  genpdflem  7874  genpdisj  7890  genpassl  7891  genpassu  7892  ltnqpri  7961  ltpopr  7962  ltexprlemm  7967  ltexprlemdisj  7973  ltexprlemloc  7974  ltrennb  8221  letri3  8406  letr  8408  ltneg  8791  leneg  8794  reapltxor  8919  apsym  8936  suprnubex  9285  suprleubex  9286  elnnnn0  9610  fcdmnn0fsupp  9620  zrevaddcl  9699  znnsub  9700  znn0sub  9714  prime  9749  eluz2  9936  eluz2b1  10010  nn01to3  10026  qrevaddcl  10053  xrletri3  10216  xrletr  10220  iccid  10337  elicopnf  10381  fzsplit2  10465  fzsplit3  10468  fzsn  10482  fzpr  10494  uzsplit  10509  fvinim0ffz  10670  lt2sqi  11077  le2sqi  11078  sseqn  11293  hashf1lem1  11299  ccatlcan  11504  ccatrcan  11505  abs00ap  11842  iooinsup  12059  mertenslem2  12319  fprod2dlemstep  12405  gcddiv  12812  algcvgblem  12843  isprm3  12912  dvdsfi  13037  ballotfilemodife  13289  imasmnd2  13808  imasgrp2  13962  issubg  14025  resgrpisgrp  14047  eqgval  14075  imasrng  14304  ring1  14413  imasring  14418  crngunit  14467  lssle0  14758  lssats2  14800  zndvds  15033  znleval  15037  znleval2  15038  eltg2b  15204  discld  15286  opnssneib  15306  restbasg  15318  ssidcn  15360  cnptoprest2  15390  lmss  15396  txrest  15426  txlm  15429  imasnopn  15449  bldisj  15551  xmeter  15586  bl2ioo  15700  limcdifap  15812  issubgr  16596  bj-sseq  16918  nnti  17120  pw1nct  17131