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  905  ifpnst  997  3anibar  1192  xor2dc  1435  bilukdc  1441  snelpwg  4308  prelpw  4311  reuhypd  4574  opelresi  5030  iota1  5308  funbrfv2b  5699  dffn5im  5700  fneqeql  5764  f1ompt  5806  dff13  5919  fliftcnv  5946  isotr  5967  isoini  5969  caovord3  6206  releldm2  6357  tpostpos  6473  nnsssuc  6713  nnaordi  6719  iserd  6771  ecdmn0m  6789  qliftel  6827  qliftfun  6829  qliftf  6832  ecopovsym  6843  pw2f1odclem  7063  mapen  7075  supisolem  7250  cnvti  7261  omp1eomlem  7336  ctssdc  7355  isomnimap  7379  ismkvmap  7396  iswomnimap  7408  netap  7516  2omotaplemap  7519  recmulnqg  7654  nqtri3or  7659  ltmnqg  7664  mullocprlem  7833  addextpr  7884  gt0srpr  8011  ltsosr  8027  ltasrg  8033  map2psrprg  8068  xrlenlt  8286  letri3  8302  subadd  8424  ltsubadd2  8655  lesubadd2  8657  suble  8662  ltsub23  8664  ltaddpos2  8675  ltsubpos  8676  subge02  8700  ltaddsublt  8793  reapneg  8819  apsym  8828  apti  8844  leltap  8847  ap0gt0  8862  divmulap  8897  divmulap3  8899  rec11rap  8933  ltdiv1  9090  ltdivmul2  9100  ledivmul2  9102  ltrec  9105  suprleubex  9176  nnle1eq1  9209  avgle1  9427  avgle2  9428  nn0le0eq0  9472  znnnlt1  9571  zleltp1  9579  elz2  9595  uzm1  9831  uzin  9833  difrp  9971  xrletri3  10083  xgepnf  10095  xltnegi  10114  xltadd1  10155  xposdif  10161  xleaddadd  10166  elioo5  10212  elfz5  10297  fzdifsuc  10361  elfzm11  10371  uzsplit  10372  elfzonelfzo  10521  qtri3or  10546  qavgle  10564  flqbi  10596  flqbi2  10597  fldiv4lem1div2uz2  10612  zmodid2  10660  q2submod  10693  sqap0  10914  lt2sq  10921  le2sq  10922  nn0opthlem1d  11028  bcval5  11071  zfz1isolemiso  11149  pfxsuffeqwrdeq  11328  shftfib  11446  mulreap  11487  caucvgrelemcau  11603  caucvgre  11604  elicc4abs  11717  abs2difabs  11731  cau4  11739  maxclpr  11845  negfi  11851  lemininf  11857  mul0inf  11864  xrlemininf  11894  xrminltinf  11895  clim2  11906  climeq  11922  fisumss  12016  fsumabs  12089  isumshft  12114  absefib  12395  dvdsval3  12415  dvdslelemd  12467  dvdsabseq  12471  dvdsflip  12475  dvdsssfz1  12476  zeo3  12492  ndvdsadd  12555  bitscmp  12582  dvdssq  12665  algcvgblem  12684  lcmdvds  12714  ncoprmgcdgt1b  12725  isprm3  12753  phiprmpw  12857  prmdiv  12870  pc11  12967  pcz  12968  pockthlem  12992  1arith  13003  ercpbllemg  13476  grpinvcnv  13714  eqger  13874  ablsubadd  13962  dvdsr02  14183  opprunitd  14188  unitsubm  14197  issubrg3  14325  aprval  14361  rnglidlmmgm  14575  znleval2  14733  discld  14930  isneip  14940  restopnb  14975  restopn2  14977  restdis  14978  lmbr2  15008  cnptoprest  15033  cnptoprest2  15034  tx1cn  15063  tx2cn  15064  txcnmpt  15067  txrest  15070  elbl2ps  15186  elbl2  15187  blcomps  15190  blcom  15191  xblpnfps  15192  xblpnf  15193  blpnf  15194  xmeter  15230  bdxmet  15295  metrest  15300  xmetxp  15301  metcn  15308  cncfcdm  15376  reefiso  15571  gausslemma2dlem0c  15853  lgseisenlem3  15874  lgsquadlem1  15879  m1lgs  15887  2lgsoddprmlem2  15908  ausgrusgrben  16092  eupth2lemsfi  16402