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  613  imordc  902  ifpnst  994  3anibar  1189  xor2dc  1432  bilukdc  1438  snelpwg  4300  prelpw  4303  reuhypd  4566  opelresi  5022  iota1  5299  funbrfv2b  5686  dffn5im  5687  fneqeql  5751  f1ompt  5794  dff13  5904  fliftcnv  5931  isotr  5952  isoini  5954  caovord3  6191  releldm2  6343  tpostpos  6425  nnsssuc  6665  nnaordi  6671  iserd  6723  ecdmn0m  6741  qliftel  6779  qliftfun  6781  qliftf  6784  ecopovsym  6795  pw2f1odclem  7015  mapen  7027  supisolem  7198  cnvti  7209  omp1eomlem  7284  ctssdc  7303  isomnimap  7327  ismkvmap  7344  iswomnimap  7356  netap  7463  2omotaplemap  7466  recmulnqg  7601  nqtri3or  7606  ltmnqg  7611  mullocprlem  7780  addextpr  7831  gt0srpr  7958  ltsosr  7974  ltasrg  7980  map2psrprg  8015  xrlenlt  8234  letri3  8250  subadd  8372  ltsubadd2  8603  lesubadd2  8605  suble  8610  ltsub23  8612  ltaddpos2  8623  ltsubpos  8624  subge02  8648  ltaddsublt  8741  reapneg  8767  apsym  8776  apti  8792  leltap  8795  ap0gt0  8810  divmulap  8845  divmulap3  8847  rec11rap  8881  ltdiv1  9038  ltdivmul2  9048  ledivmul2  9050  ltrec  9053  suprleubex  9124  nnle1eq1  9157  avgle1  9375  avgle2  9376  nn0le0eq0  9420  znnnlt1  9517  zleltp1  9525  elz2  9541  uzm1  9777  uzin  9779  difrp  9917  xrletri3  10029  xgepnf  10041  xltnegi  10060  xltadd1  10101  xposdif  10107  xleaddadd  10112  elioo5  10158  elfz5  10242  fzdifsuc  10306  elfzm11  10316  uzsplit  10317  elfzonelfzo  10465  qtri3or  10490  qavgle  10508  flqbi  10540  flqbi2  10541  fldiv4lem1div2uz2  10556  zmodid2  10604  q2submod  10637  sqap0  10858  lt2sq  10865  le2sq  10866  nn0opthlem1d  10972  bcval5  11015  zfz1isolemiso  11093  pfxsuffeqwrdeq  11269  shftfib  11374  mulreap  11415  caucvgrelemcau  11531  caucvgre  11532  elicc4abs  11645  abs2difabs  11659  cau4  11667  maxclpr  11773  negfi  11779  lemininf  11785  mul0inf  11792  xrlemininf  11822  xrminltinf  11823  clim2  11834  climeq  11850  fisumss  11943  fsumabs  12016  isumshft  12041  absefib  12322  dvdsval3  12342  dvdslelemd  12394  dvdsabseq  12398  dvdsflip  12402  dvdsssfz1  12403  zeo3  12419  ndvdsadd  12482  bitscmp  12509  dvdssq  12592  algcvgblem  12611  lcmdvds  12641  ncoprmgcdgt1b  12652  isprm3  12680  phiprmpw  12784  prmdiv  12797  pc11  12894  pcz  12895  pockthlem  12919  1arith  12930  ercpbllemg  13403  grpinvcnv  13641  eqger  13801  ablsubadd  13889  dvdsr02  14109  opprunitd  14114  unitsubm  14123  issubrg3  14251  aprval  14286  rnglidlmmgm  14500  znleval2  14658  discld  14850  isneip  14860  restopnb  14895  restopn2  14897  restdis  14898  lmbr2  14928  cnptoprest  14953  cnptoprest2  14954  tx1cn  14983  tx2cn  14984  txcnmpt  14987  txrest  14990  elbl2ps  15106  elbl2  15107  blcomps  15110  blcom  15111  xblpnfps  15112  xblpnf  15113  blpnf  15114  xmeter  15150  bdxmet  15215  metrest  15220  xmetxp  15221  metcn  15228  cncfcdm  15296  reefiso  15491  gausslemma2dlem0c  15770  lgseisenlem3  15791  lgsquadlem1  15796  m1lgs  15804  2lgsoddprmlem2  15825  ausgrusgrben  16007