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  4503  opelresi  4954  iota1  5230  funbrfv2b  5602  dffn5im  5603  fneqeql  5667  f1ompt  5710  dff13  5812  fliftcnv  5839  isotr  5860  isoini  5862  caovord3  6094  releldm2  6240  tpostpos  6319  nnsssuc  6557  nnaordi  6563  iserd  6615  ecdmn0m  6633  qliftel  6671  qliftfun  6673  qliftf  6676  ecopovsym  6687  pw2f1odclem  6892  mapen  6904  supisolem  7069  cnvti  7080  omp1eomlem  7155  ctssdc  7174  isomnimap  7198  ismkvmap  7215  iswomnimap  7227  netap  7316  2omotaplemap  7319  recmulnqg  7453  nqtri3or  7458  ltmnqg  7463  mullocprlem  7632  addextpr  7683  gt0srpr  7810  ltsosr  7826  ltasrg  7832  map2psrprg  7867  xrlenlt  8086  letri3  8102  subadd  8224  ltsubadd2  8454  lesubadd2  8456  suble  8461  ltsub23  8463  ltaddpos2  8474  ltsubpos  8475  subge02  8499  ltaddsublt  8592  reapneg  8618  apsym  8627  apti  8643  leltap  8646  ap0gt0  8661  divmulap  8696  divmulap3  8698  rec11rap  8732  ltdiv1  8889  ltdivmul2  8899  ledivmul2  8901  ltrec  8904  suprleubex  8975  nnle1eq1  9008  avgle1  9226  avgle2  9227  nn0le0eq0  9271  znnnlt1  9368  zleltp1  9375  elz2  9391  uzm1  9626  uzin  9628  difrp  9761  xrletri3  9873  xgepnf  9885  xltnegi  9904  xltadd1  9945  xposdif  9951  xleaddadd  9956  elioo5  10002  elfz5  10086  fzdifsuc  10150  elfzm11  10160  uzsplit  10161  elfzonelfzo  10300  qtri3or  10313  qavgle  10330  flqbi  10362  flqbi2  10363  fldiv4lem1div2uz2  10378  zmodid2  10426  q2submod  10459  sqap0  10680  lt2sq  10687  le2sq  10688  nn0opthlem1d  10794  bcval5  10837  zfz1isolemiso  10913  shftfib  10970  mulreap  11011  caucvgrelemcau  11127  caucvgre  11128  elicc4abs  11241  abs2difabs  11255  cau4  11263  maxclpr  11369  negfi  11374  lemininf  11380  mul0inf  11387  xrlemininf  11417  xrminltinf  11418  clim2  11429  climeq  11445  fisumss  11538  fsumabs  11611  isumshft  11636  absefib  11917  dvdsval3  11937  dvdslelemd  11988  dvdsabseq  11992  dvdsflip  11996  dvdsssfz1  11997  zeo3  12012  ndvdsadd  12075  dvdssq  12171  algcvgblem  12190  lcmdvds  12220  ncoprmgcdgt1b  12231  isprm3  12259  phiprmpw  12363  prmdiv  12376  pc11  12472  pcz  12473  pockthlem  12497  1arith  12508  ercpbllemg  12916  grpinvcnv  13143  eqger  13297  ablsubadd  13385  dvdsr02  13604  opprunitd  13609  unitsubm  13618  issubrg3  13746  aprval  13781  rnglidlmmgm  13995  znleval2  14153  discld  14315  isneip  14325  restopnb  14360  restopn2  14362  restdis  14363  lmbr2  14393  cnptoprest  14418  cnptoprest2  14419  tx1cn  14448  tx2cn  14449  txcnmpt  14452  txrest  14455  elbl2ps  14571  elbl2  14572  blcomps  14575  blcom  14576  xblpnfps  14577  xblpnf  14578  blpnf  14579  xmeter  14615  bdxmet  14680  metrest  14685  xmetxp  14686  metcn  14693  cncfcdm  14761  reefiso  14953  gausslemma2dlem0c  15208  lgseisenlem3  15229  lgsquadlem1  15234  m1lgs  15242  2lgsoddprmlem2  15263