Theorem bitr4d 190

Description: Deduction form of bitr4i 186. (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 140	. 2 |- ( ph -> ( ch <-> th ) )
4	1, 3	bitrd 187	1 |- ( ph -> ( ps <-> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitr2d  215  3bitr2rd  216  3bitr4d  219  3bitr4rd  220  mpbirand  438  mpbiran2d  439  bianabs  601  imordc  883  3anibar  1150  xor2dc  1369  bilukdc  1375  reuhypd  4400  opelresi  4838  iota1  5110  funbrfv2b  5474  dffn5im  5475  fneqeql  5536  f1ompt  5579  dff13  5677  fliftcnv  5704  isotr  5725  isoini  5727  caovord3  5952  releldm2  6091  tpostpos  6169  nnsssuc  6406  nnaordi  6412  iserd  6463  ecdmn0m  6479  qliftel  6517  qliftfun  6519  qliftf  6522  ecopovsym  6533  mapen  6748  supisolem  6903  cnvti  6914  omp1eomlem  6987  ctssdc  7006  isomnimap  7017  ismkvmap  7036  iswomnimap  7048  recmulnqg  7223  nqtri3or  7228  ltmnqg  7233  mullocprlem  7402  addextpr  7453  gt0srpr  7580  ltsosr  7596  ltasrg  7602  map2psrprg  7637  xrlenlt  7853  letri3  7869  subadd  7989  ltsubadd2  8219  lesubadd2  8221  suble  8226  ltsub23  8228  ltaddpos2  8239  ltsubpos  8240  subge02  8264  ltaddsublt  8357  reapneg  8383  apsym  8392  apti  8408  leltap  8411  ap0gt0  8426  divmulap  8459  divmulap3  8461  rec11rap  8495  ltdiv1  8650  ltdivmul2  8660  ledivmul2  8662  ltrec  8665  suprleubex  8736  nnle1eq1  8768  avgle1  8984  avgle2  8985  nn0le0eq0  9029  znnnlt1  9126  zleltp1  9133  elz2  9146  uzm1  9380  uzin  9382  difrp  9509  xrletri3  9618  xgepnf  9629  xltnegi  9648  xltadd1  9689  xposdif  9695  xleaddadd  9700  elioo5  9746  elfz5  9829  fzdifsuc  9892  elfzm11  9902  uzsplit  9903  elfzonelfzo  10038  qtri3or  10051  qavgle  10067  flqbi  10094  flqbi2  10095  zmodid2  10156  q2submod  10189  sqap0  10390  lt2sq  10397  le2sq  10398  nn0opthlem1d  10498  bcval5  10541  zfz1isolemiso  10614  shftfib  10627  mulreap  10668  caucvgrelemcau  10784  caucvgre  10785  elicc4abs  10898  abs2difabs  10912  cau4  10920  maxclpr  11026  negfi  11031  lemininf  11037  mul0inf  11044  xrlemininf  11072  xrminltinf  11073  clim2  11084  climeq  11100  fisumss  11193  fsumabs  11266  isumshft  11291  absefib  11513  dvdsval3  11533  dvdslelemd  11577  dvdsabseq  11581  dvdsflip  11585  dvdsssfz1  11586  zeo3  11601  ndvdsadd  11664  dvdssq  11755  algcvgblem  11766  lcmdvds  11796  ncoprmgcdgt1b  11807  isprm3  11835  phiprmpw  11934  discld  12344  isneip  12354  restopnb  12389  restopn2  12391  restdis  12392  lmbr2  12422  cnptoprest  12447  cnptoprest2  12448  tx1cn  12477  tx2cn  12478  txcnmpt  12481  txrest  12484  elbl2ps  12600  elbl2  12601  blcomps  12604  blcom  12605  xblpnfps  12606  xblpnf  12607  blpnf  12608  xmeter  12644  bdxmet  12709  metrest  12714  xmetxp  12715  metcn  12722  cncffvrn  12777  reefiso  12906