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  898  3anibar  1167  xor2dc  1401  bilukdc  1407  reuhypd  4506  opelresi  4957  iota1  5233  funbrfv2b  5605  dffn5im  5606  fneqeql  5670  f1ompt  5713  dff13  5815  fliftcnv  5842  isotr  5863  isoini  5865  caovord3  6097  releldm2  6243  tpostpos  6322  nnsssuc  6560  nnaordi  6566  iserd  6618  ecdmn0m  6636  qliftel  6674  qliftfun  6676  qliftf  6679  ecopovsym  6690  pw2f1odclem  6895  mapen  6907  supisolem  7074  cnvti  7085  omp1eomlem  7160  ctssdc  7179  isomnimap  7203  ismkvmap  7220  iswomnimap  7232  netap  7321  2omotaplemap  7324  recmulnqg  7458  nqtri3or  7463  ltmnqg  7468  mullocprlem  7637  addextpr  7688  gt0srpr  7815  ltsosr  7831  ltasrg  7837  map2psrprg  7872  xrlenlt  8091  letri3  8107  subadd  8229  ltsubadd2  8460  lesubadd2  8462  suble  8467  ltsub23  8469  ltaddpos2  8480  ltsubpos  8481  subge02  8505  ltaddsublt  8598  reapneg  8624  apsym  8633  apti  8649  leltap  8652  ap0gt0  8667  divmulap  8702  divmulap3  8704  rec11rap  8738  ltdiv1  8895  ltdivmul2  8905  ledivmul2  8907  ltrec  8910  suprleubex  8981  nnle1eq1  9014  avgle1  9232  avgle2  9233  nn0le0eq0  9277  znnnlt1  9374  zleltp1  9381  elz2  9397  uzm1  9632  uzin  9634  difrp  9767  xrletri3  9879  xgepnf  9891  xltnegi  9910  xltadd1  9951  xposdif  9957  xleaddadd  9962  elioo5  10008  elfz5  10092  fzdifsuc  10156  elfzm11  10166  uzsplit  10167  elfzonelfzo  10306  qtri3or  10330  qavgle  10348  flqbi  10380  flqbi2  10381  fldiv4lem1div2uz2  10396  zmodid2  10444  q2submod  10477  sqap0  10698  lt2sq  10705  le2sq  10706  nn0opthlem1d  10812  bcval5  10855  zfz1isolemiso  10931  shftfib  10988  mulreap  11029  caucvgrelemcau  11145  caucvgre  11146  elicc4abs  11259  abs2difabs  11273  cau4  11281  maxclpr  11387  negfi  11393  lemininf  11399  mul0inf  11406  xrlemininf  11436  xrminltinf  11437  clim2  11448  climeq  11464  fisumss  11557  fsumabs  11630  isumshft  11655  absefib  11936  dvdsval3  11956  dvdslelemd  12008  dvdsabseq  12012  dvdsflip  12016  dvdsssfz1  12017  zeo3  12033  ndvdsadd  12096  dvdssq  12198  algcvgblem  12217  lcmdvds  12247  ncoprmgcdgt1b  12258  isprm3  12286  phiprmpw  12390  prmdiv  12403  pc11  12500  pcz  12501  pockthlem  12525  1arith  12536  ercpbllemg  12973  grpinvcnv  13200  eqger  13354  ablsubadd  13442  dvdsr02  13661  opprunitd  13666  unitsubm  13675  issubrg3  13803  aprval  13838  rnglidlmmgm  14052  znleval2  14210  discld  14372  isneip  14382  restopnb  14417  restopn2  14419  restdis  14420  lmbr2  14450  cnptoprest  14475  cnptoprest2  14476  tx1cn  14505  tx2cn  14506  txcnmpt  14509  txrest  14512  elbl2ps  14628  elbl2  14629  blcomps  14632  blcom  14633  xblpnfps  14634  xblpnf  14635  blpnf  14636  xmeter  14672  bdxmet  14737  metrest  14742  xmetxp  14743  metcn  14750  cncfcdm  14818  reefiso  15013  gausslemma2dlem0c  15292  lgseisenlem3  15313  lgsquadlem1  15318  m1lgs  15326  2lgsoddprmlem2  15347