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  897  3anibar  1165  xor2dc  1390  bilukdc  1396  reuhypd  4471  opelresi  4918  iota1  5192  funbrfv2b  5560  dffn5im  5561  fneqeql  5624  f1ompt  5667  dff13  5768  fliftcnv  5795  isotr  5816  isoini  5818  caovord3  6047  releldm2  6185  tpostpos  6264  nnsssuc  6502  nnaordi  6508  iserd  6560  ecdmn0m  6576  qliftel  6614  qliftfun  6616  qliftf  6619  ecopovsym  6630  mapen  6845  supisolem  7006  cnvti  7017  omp1eomlem  7092  ctssdc  7111  isomnimap  7134  ismkvmap  7151  iswomnimap  7163  netap  7252  2omotaplemap  7255  recmulnqg  7389  nqtri3or  7394  ltmnqg  7399  mullocprlem  7568  addextpr  7619  gt0srpr  7746  ltsosr  7762  ltasrg  7768  map2psrprg  7803  xrlenlt  8021  letri3  8037  subadd  8159  ltsubadd2  8389  lesubadd2  8391  suble  8396  ltsub23  8398  ltaddpos2  8409  ltsubpos  8410  subge02  8434  ltaddsublt  8527  reapneg  8553  apsym  8562  apti  8578  leltap  8581  ap0gt0  8596  divmulap  8631  divmulap3  8633  rec11rap  8667  ltdiv1  8824  ltdivmul2  8834  ledivmul2  8836  ltrec  8839  suprleubex  8910  nnle1eq1  8942  avgle1  9158  avgle2  9159  nn0le0eq0  9203  znnnlt1  9300  zleltp1  9307  elz2  9323  uzm1  9557  uzin  9559  difrp  9691  xrletri3  9803  xgepnf  9815  xltnegi  9834  xltadd1  9875  xposdif  9881  xleaddadd  9886  elioo5  9932  elfz5  10016  fzdifsuc  10080  elfzm11  10090  uzsplit  10091  elfzonelfzo  10229  qtri3or  10242  qavgle  10258  flqbi  10289  flqbi2  10290  zmodid2  10351  q2submod  10384  sqap0  10586  lt2sq  10593  le2sq  10594  nn0opthlem1d  10699  bcval5  10742  zfz1isolemiso  10818  shftfib  10831  mulreap  10872  caucvgrelemcau  10988  caucvgre  10989  elicc4abs  11102  abs2difabs  11116  cau4  11124  maxclpr  11230  negfi  11235  lemininf  11241  mul0inf  11248  xrlemininf  11278  xrminltinf  11279  clim2  11290  climeq  11306  fisumss  11399  fsumabs  11472  isumshft  11497  absefib  11777  dvdsval3  11797  dvdslelemd  11848  dvdsabseq  11852  dvdsflip  11856  dvdsssfz1  11857  zeo3  11872  ndvdsadd  11935  dvdssq  12031  algcvgblem  12048  lcmdvds  12078  ncoprmgcdgt1b  12089  isprm3  12117  phiprmpw  12221  prmdiv  12234  pc11  12329  pcz  12330  pockthlem  12353  1arith  12364  ercpbllemg  12748  grpinvcnv  12937  eqger  13081  ablsubadd  13113  dvdsr02  13272  opprunitd  13277  unitsubm  13286  issubrg3  13366  aprval  13370  discld  13606  isneip  13616  restopnb  13651  restopn2  13653  restdis  13654  lmbr2  13684  cnptoprest  13709  cnptoprest2  13710  tx1cn  13739  tx2cn  13740  txcnmpt  13743  txrest  13746  elbl2ps  13862  elbl2  13863  blcomps  13866  blcom  13867  xblpnfps  13868  xblpnf  13869  blpnf  13870  xmeter  13906  bdxmet  13971  metrest  13976  xmetxp  13977  metcn  13984  cncfcdm  14039  reefiso  14168  m1lgs  14422  2lgsoddprmlem2  14424