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  1393  3biant1d  1396  equsalh  1778  eueq3dc  3000  sbcel12g  3162  sbceqg  3163  sbcnel12g  3164  reldisj  3575  r19.3rm  3613  eldifpr  3732  eldiftp  3751  rabxp  4807  elrng  4966  iss  5104  eliniseg  5152  fcnvres  5570  dffv3g  5686  funimass4  5747  fndmdif  5805  fneqeql  5808  funimass3  5816  elrnrexdmb  5839  dff4im  5845  fconst4m  5926  elunirn  5962  riota1  6048  riota2df  6050  f1ocnvfv3  6064  eqfnov  6185  caoftrn  6325  suppimacnvfn  6476  suppssrst  6491  suppssrgst  6492  mpoxopovel  6502  rntpos  6518  ordgt0ge1  6698  iinerm  6871  erinxp  6873  qliftfun  6881  mapdm0  6927  elfi2  7296  fifo  7304  2omap  7308  inl11  7395  ctssdccl  7441  isomnimap  7467  ismkvmap  7484  iswomnimap  7496  omniwomnimkv  7497  pr2nelem  7527  indpi  7699  genpdflem  7864  genpdisj  7880  genpassl  7881  genpassu  7882  ltnqpri  7951  ltpopr  7952  ltexprlemm  7957  ltexprlemdisj  7963  ltexprlemloc  7964  ltrennb  8211  letri3  8396  letr  8398  ltneg  8780  leneg  8783  reapltxor  8907  apsym  8924  suprnubex  9273  suprleubex  9274  elnnnn0  9585  fcdmnn0fsupp  9595  zrevaddcl  9674  znnsub  9675  znn0sub  9689  prime  9724  eluz2  9906  eluz2b1  9980  nn01to3  9996  qrevaddcl  10023  xrletri3  10185  xrletr  10189  iccid  10306  elicopnf  10350  fzsplit2  10433  fzsplit3  10436  fzsn  10450  fzpr  10462  uzsplit  10477  fvinim0ffz  10638  lt2sqi  11042  le2sqi  11043  sseqn  11257  hashf1lem1  11263  ccatlcan  11468  ccatrcan  11469  abs00ap  11806  iooinsup  12021  mertenslem2  12281  fprod2dlemstep  12367  gcddiv  12774  algcvgblem  12805  isprm3  12874  dvdsfi  12995  ballotfilemodife  13218  imasmnd2  13736  imasgrp2  13890  issubg  13953  resgrpisgrp  13975  eqgval  14003  imasrng  14230  ring1  14337  imasring  14342  crngunit  14391  lssle0  14681  lssats2  14723  zndvds  14956  znleval  14960  znleval2  14961  eltg2b  15078  discld  15160  opnssneib  15180  restbasg  15192  ssidcn  15234  cnptoprest2  15264  lmss  15270  txrest  15300  txlm  15303  imasnopn  15323  bldisj  15425  xmeter  15460  bl2ioo  15574  limcdifap  15686  issubgr  16412  bj-sseq  16734  nnti  16936  pw1nct  16947