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  equsalh  1740  eueq3dc  2938  sbcel12g  3099  sbceqg  3100  sbcnel12g  3101  reldisj  3502  r19.3rm  3539  eldifpr  3649  eldiftp  3668  rabxp  4700  elrng  4857  iss  4992  eliniseg  5039  fcnvres  5441  dffv3g  5554  funimass4  5611  fndmdif  5667  fneqeql  5670  funimass3  5678  elrnrexdmb  5702  dff4im  5708  fconst4m  5782  elunirn  5813  riota1  5896  riota2df  5898  f1ocnvfv3  5911  eqfnov  6029  caoftrn  6163  mpoxopovel  6299  rntpos  6315  ordgt0ge1  6493  iinerm  6666  erinxp  6668  qliftfun  6676  mapdm0  6722  elfi2  7038  fifo  7046  inl11  7131  ctssdccl  7177  isomnimap  7203  ismkvmap  7220  iswomnimap  7232  omniwomnimkv  7233  pr2nelem  7258  indpi  7409  genpdflem  7574  genpdisj  7590  genpassl  7591  genpassu  7592  ltnqpri  7661  ltpopr  7662  ltexprlemm  7667  ltexprlemdisj  7673  ltexprlemloc  7674  ltrennb  7921  letri3  8107  letr  8109  ltneg  8489  leneg  8492  reapltxor  8616  apsym  8633  suprnubex  8980  suprleubex  8981  elnnnn0  9292  zrevaddcl  9376  znnsub  9377  znn0sub  9391  prime  9425  eluz2  9607  eluz2b1  9675  nn01to3  9691  qrevaddcl  9718  xrletri3  9879  xrletr  9883  iccid  10000  elicopnf  10044  fzsplit2  10125  fzsn  10141  fzpr  10152  uzsplit  10167  fvinim0ffz  10317  lt2sqi  10719  le2sqi  10720  abs00ap  11227  iooinsup  11442  mertenslem2  11701  fprod2dlemstep  11787  gcddiv  12186  algcvgblem  12217  isprm3  12286  dvdsfi  12407  imasgrp2  13240  issubg  13303  resgrpisgrp  13325  eqgval  13353  imasrng  13512  ring1  13615  imasring  13620  crngunit  13667  lssle0  13928  lssats2  13970  zndvds  14205  znleval  14209  znleval2  14210  eltg2b  14290  discld  14372  opnssneib  14392  restbasg  14404  ssidcn  14446  cnptoprest2  14476  lmss  14482  txrest  14512  txlm  14515  imasnopn  14535  bldisj  14637  xmeter  14672  bl2ioo  14786  limcdifap  14898  bj-sseq  15438  nnti  15639  pw1nct  15647