Theorem bitr4d 191

Description: Deduction form of bitr4i 187. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr4d.1	|- ( ph -> ( ps <-> ch ) )
bitr4d.2	|- ( ph -> ( th <-> ch ) )

Assertion

Ref	Expression
bitr4d	|- ( ph -> ( ps <-> th ) )

Proof of Theorem bitr4d

Step	Hyp	Ref	Expression
1		bitr4d.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		bitr4d.2	. . 3 |- ( ph -> ( th <-> ch ) )
3	2	bicomd 141	. 2 |- ( ph -> ( ch <-> th ) )
4	1, 3	bitrd 188	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:  3bitr2d  216  3bitr2rd  217  3bitr4d  220  3bitr4rd  221  mpbirand  441  mpbiran2d  442  bianabs  611  imordc  899  3anibar  1168  xor2dc  1410  bilukdc  1416  reuhypd  4526  opelresi  4979  iota1  5255  funbrfv2b  5636  dffn5im  5637  fneqeql  5701  f1ompt  5744  dff13  5850  fliftcnv  5877  isotr  5898  isoini  5900  caovord3  6133  releldm2  6284  tpostpos  6363  nnsssuc  6601  nnaordi  6607  iserd  6659  ecdmn0m  6677  qliftel  6715  qliftfun  6717  qliftf  6720  ecopovsym  6731  pw2f1odclem  6946  mapen  6958  supisolem  7125  cnvti  7136  omp1eomlem  7211  ctssdc  7230  isomnimap  7254  ismkvmap  7271  iswomnimap  7283  netap  7386  2omotaplemap  7389  recmulnqg  7524  nqtri3or  7529  ltmnqg  7534  mullocprlem  7703  addextpr  7754  gt0srpr  7881  ltsosr  7897  ltasrg  7903  map2psrprg  7938  xrlenlt  8157  letri3  8173  subadd  8295  ltsubadd2  8526  lesubadd2  8528  suble  8533  ltsub23  8535  ltaddpos2  8546  ltsubpos  8547  subge02  8571  ltaddsublt  8664  reapneg  8690  apsym  8699  apti  8715  leltap  8718  ap0gt0  8733  divmulap  8768  divmulap3  8770  rec11rap  8804  ltdiv1  8961  ltdivmul2  8971  ledivmul2  8973  ltrec  8976  suprleubex  9047  nnle1eq1  9080  avgle1  9298  avgle2  9299  nn0le0eq0  9343  znnnlt1  9440  zleltp1  9448  elz2  9464  uzm1  9699  uzin  9701  difrp  9834  xrletri3  9946  xgepnf  9958  xltnegi  9977  xltadd1  10018  xposdif  10024  xleaddadd  10029  elioo5  10075  elfz5  10159  fzdifsuc  10223  elfzm11  10233  uzsplit  10234  elfzonelfzo  10381  qtri3or  10405  qavgle  10423  flqbi  10455  flqbi2  10456  fldiv4lem1div2uz2  10471  zmodid2  10519  q2submod  10552  sqap0  10773  lt2sq  10780  le2sq  10781  nn0opthlem1d  10887  bcval5  10930  zfz1isolemiso  11006  pfxsuffeqwrdeq  11174  shftfib  11209  mulreap  11250  caucvgrelemcau  11366  caucvgre  11367  elicc4abs  11480  abs2difabs  11494  cau4  11502  maxclpr  11608  negfi  11614  lemininf  11620  mul0inf  11627  xrlemininf  11657  xrminltinf  11658  clim2  11669  climeq  11685  fisumss  11778  fsumabs  11851  isumshft  11876  absefib  12157  dvdsval3  12177  dvdslelemd  12229  dvdsabseq  12233  dvdsflip  12237  dvdsssfz1  12238  zeo3  12254  ndvdsadd  12317  bitscmp  12344  dvdssq  12427  algcvgblem  12446  lcmdvds  12476  ncoprmgcdgt1b  12487  isprm3  12515  phiprmpw  12619  prmdiv  12632  pc11  12729  pcz  12730  pockthlem  12754  1arith  12765  ercpbllemg  13237  grpinvcnv  13475  eqger  13635  ablsubadd  13723  dvdsr02  13942  opprunitd  13947  unitsubm  13956  issubrg3  14084  aprval  14119  rnglidlmmgm  14333  znleval2  14491  discld  14683  isneip  14693  restopnb  14728  restopn2  14730  restdis  14731  lmbr2  14761  cnptoprest  14786  cnptoprest2  14787  tx1cn  14816  tx2cn  14817  txcnmpt  14820  txrest  14823  elbl2ps  14939  elbl2  14940  blcomps  14943  blcom  14944  xblpnfps  14945  xblpnf  14946  blpnf  14947  xmeter  14983  bdxmet  15048  metrest  15053  xmetxp  15054  metcn  15061  cncfcdm  15129  reefiso  15324  gausslemma2dlem0c  15603  lgseisenlem3  15624  lgsquadlem1  15629  m1lgs  15637  2lgsoddprmlem2  15658