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  4814  elrng  4973  iss  5112  eliniseg  5160  fcnvres  5578  dffv3g  5694  funimass4  5756  fndmdif  5817  fneqeql  5820  funimass3  5828  elrnrexdmb  5851  dff4im  5857  fconst4m  5938  elunirn  5975  riota1  6061  riota2df  6063  f1ocnvfv3  6077  eqfnov  6198  caoftrn  6339  suppimacnvfn  6490  suppssrst  6505  suppssrgst  6506  mpoxopovel  6517  rntpos  6533  ordgt0ge1  6713  iinerm  6886  erinxp  6888  qliftfun  6896  mapdm0  6942  relresfin  7270  elfi2  7311  fifo  7319  2omap  7324  inl11  7411  ctssdccl  7457  isomnimap  7483  ismkvmap  7500  iswomnimap  7512  omniwomnimkv  7513  pr2nelem  7543  indpi  7715  genpdflem  7880  genpdisj  7896  genpassl  7897  genpassu  7898  ltnqpri  7967  ltpopr  7968  ltexprlemm  7973  ltexprlemdisj  7979  ltexprlemloc  7980  ltrennb  8227  letri3  8412  letr  8414  ltneg  8797  leneg  8800  reapltxor  8925  apsym  8942  suprnubex  9291  suprleubex  9292  elnnnn0  9617  zrevaddcl  9704  znnsub  9705  znn0sub  9719  prime  9755  eluz2  9942  eluz2b1  10016  nn01to3  10032  qrevaddcl  10059  xrletri3  10222  xrletr  10226  iccid  10343  elicopnf  10387  fzsplit2  10471  fzsplit3  10474  fzsn  10488  fzpr  10500  uzsplit  10515  fvinim0ffz  10676  lt2sqi  11084  le2sqi  11085  sseqn  11300  hashf1lem1  11306  ccatlcan  11511  ccatrcan  11512  abs00ap  11849  iooinsup  12067  mertenslem2  12327  fprod2dlemstep  12413  gcddiv  12820  algcvgblem  12851  isprm3  12920  dvdsfi  13045  ballotfilemodife  13297  imasmnd2  13817  imasgrp2  13971  issubg  14034  resgrpisgrp  14056  eqgval  14084  gsumcom2fi  14274  imasrng  14361  ring1  14470  imasring  14477  crngunit  14526  lssle0  14817  lssats2  14859  zndvds  15092  znleval  15096  znleval2  15097  eltg2b  15297  discld  15379  opnssneib  15399  restbasg  15411  ssidcn  15453  cnptoprest2  15483  lmss  15489  txrest  15519  txlm  15522  imasnopn  15542  bldisj  15644  xmeter  15679  bl2ioo  15793  limcdifap  15905  bposlem6  16333  issubgr  16720  bj-sseq  17042  nnti  17244  pw1nct  17255