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  615  imordc  904  ifpnst  996  3anibar  1191  xor2dc  1434  bilukdc  1440  snelpwg  4302  prelpw  4305  reuhypd  4568  opelresi  5024  iota1  5301  funbrfv2b  5690  dffn5im  5691  fneqeql  5755  f1ompt  5798  dff13  5909  fliftcnv  5936  isotr  5957  isoini  5959  caovord3  6196  releldm2  6348  tpostpos  6430  nnsssuc  6670  nnaordi  6676  iserd  6728  ecdmn0m  6746  qliftel  6784  qliftfun  6786  qliftf  6789  ecopovsym  6800  pw2f1odclem  7020  mapen  7032  supisolem  7207  cnvti  7218  omp1eomlem  7293  ctssdc  7312  isomnimap  7336  ismkvmap  7353  iswomnimap  7365  netap  7473  2omotaplemap  7476  recmulnqg  7611  nqtri3or  7616  ltmnqg  7621  mullocprlem  7790  addextpr  7841  gt0srpr  7968  ltsosr  7984  ltasrg  7990  map2psrprg  8025  xrlenlt  8244  letri3  8260  subadd  8382  ltsubadd2  8613  lesubadd2  8615  suble  8620  ltsub23  8622  ltaddpos2  8633  ltsubpos  8634  subge02  8658  ltaddsublt  8751  reapneg  8777  apsym  8786  apti  8802  leltap  8805  ap0gt0  8820  divmulap  8855  divmulap3  8857  rec11rap  8891  ltdiv1  9048  ltdivmul2  9058  ledivmul2  9060  ltrec  9063  suprleubex  9134  nnle1eq1  9167  avgle1  9385  avgle2  9386  nn0le0eq0  9430  znnnlt1  9527  zleltp1  9535  elz2  9551  uzm1  9787  uzin  9789  difrp  9927  xrletri3  10039  xgepnf  10051  xltnegi  10070  xltadd1  10111  xposdif  10117  xleaddadd  10122  elioo5  10168  elfz5  10252  fzdifsuc  10316  elfzm11  10326  uzsplit  10327  elfzonelfzo  10476  qtri3or  10501  qavgle  10519  flqbi  10551  flqbi2  10552  fldiv4lem1div2uz2  10567  zmodid2  10615  q2submod  10648  sqap0  10869  lt2sq  10876  le2sq  10877  nn0opthlem1d  10983  bcval5  11026  zfz1isolemiso  11104  pfxsuffeqwrdeq  11283  shftfib  11401  mulreap  11442  caucvgrelemcau  11558  caucvgre  11559  elicc4abs  11672  abs2difabs  11686  cau4  11694  maxclpr  11800  negfi  11806  lemininf  11812  mul0inf  11819  xrlemininf  11849  xrminltinf  11850  clim2  11861  climeq  11877  fisumss  11971  fsumabs  12044  isumshft  12069  absefib  12350  dvdsval3  12370  dvdslelemd  12422  dvdsabseq  12426  dvdsflip  12430  dvdsssfz1  12431  zeo3  12447  ndvdsadd  12510  bitscmp  12537  dvdssq  12620  algcvgblem  12639  lcmdvds  12669  ncoprmgcdgt1b  12680  isprm3  12708  phiprmpw  12812  prmdiv  12825  pc11  12922  pcz  12923  pockthlem  12947  1arith  12958  ercpbllemg  13431  grpinvcnv  13669  eqger  13829  ablsubadd  13917  dvdsr02  14138  opprunitd  14143  unitsubm  14152  issubrg3  14280  aprval  14315  rnglidlmmgm  14529  znleval2  14687  discld  14879  isneip  14889  restopnb  14924  restopn2  14926  restdis  14927  lmbr2  14957  cnptoprest  14982  cnptoprest2  14983  tx1cn  15012  tx2cn  15013  txcnmpt  15016  txrest  15019  elbl2ps  15135  elbl2  15136  blcomps  15139  blcom  15140  xblpnfps  15141  xblpnf  15142  blpnf  15143  xmeter  15179  bdxmet  15244  metrest  15249  xmetxp  15250  metcn  15257  cncfcdm  15325  reefiso  15520  gausslemma2dlem0c  15799  lgseisenlem3  15820  lgsquadlem1  15825  m1lgs  15833  2lgsoddprmlem2  15854  ausgrusgrben  16038  eupth2lemsfi  16348