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  6516  rntpos  6532  ordgt0ge1  6712  iinerm  6885  erinxp  6887  qliftfun  6895  mapdm0  6941  relresfin  7268  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  fcdmnn0fsupp  9627  zrevaddcl  9706  znnsub  9707  znn0sub  9721  prime  9756  eluz2  9943  eluz2b1  10017  nn01to3  10033  qrevaddcl  10060  xrletri3  10223  xrletr  10227  iccid  10344  elicopnf  10388  fzsplit2  10472  fzsplit3  10475  fzsn  10489  fzpr  10501  uzsplit  10516  fvinim0ffz  10677  lt2sqi  11085  le2sqi  11086  sseqn  11301  hashf1lem1  11307  ccatlcan  11512  ccatrcan  11513  abs00ap  11850  iooinsup  12068  mertenslem2  12328  fprod2dlemstep  12414  gcddiv  12821  algcvgblem  12852  isprm3  12921  dvdsfi  13046  ballotfilemodife  13298  imasmnd2  13818  imasgrp2  13972  issubg  14035  resgrpisgrp  14057  eqgval  14085  gsumcom2fi  14275  imasrng  14362  ring1  14471  imasring  14478  crngunit  14527  lssle0  14818  lssats2  14860  zndvds  15093  znleval  15097  znleval2  15098  eltg2b  15280  discld  15362  opnssneib  15382  restbasg  15394  ssidcn  15436  cnptoprest2  15466  lmss  15472  txrest  15502  txlm  15505  imasnopn  15525  bldisj  15627  xmeter  15662  bl2ioo  15776  limcdifap  15888  bposlem6  16316  issubgr  16703  bj-sseq  17025  nnti  17227  pw1nct  17238