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  4296  prelpw  4299  reuhypd  4562  opelresi  5016  iota1  5293  funbrfv2b  5680  dffn5im  5681  fneqeql  5745  f1ompt  5788  dff13  5898  fliftcnv  5925  isotr  5946  isoini  5948  caovord3  6185  releldm2  6337  tpostpos  6416  nnsssuc  6656  nnaordi  6662  iserd  6714  ecdmn0m  6732  qliftel  6770  qliftfun  6772  qliftf  6775  ecopovsym  6786  pw2f1odclem  7003  mapen  7015  supisolem  7186  cnvti  7197  omp1eomlem  7272  ctssdc  7291  isomnimap  7315  ismkvmap  7332  iswomnimap  7344  netap  7451  2omotaplemap  7454  recmulnqg  7589  nqtri3or  7594  ltmnqg  7599  mullocprlem  7768  addextpr  7819  gt0srpr  7946  ltsosr  7962  ltasrg  7968  map2psrprg  8003  xrlenlt  8222  letri3  8238  subadd  8360  ltsubadd2  8591  lesubadd2  8593  suble  8598  ltsub23  8600  ltaddpos2  8611  ltsubpos  8612  subge02  8636  ltaddsublt  8729  reapneg  8755  apsym  8764  apti  8780  leltap  8783  ap0gt0  8798  divmulap  8833  divmulap3  8835  rec11rap  8869  ltdiv1  9026  ltdivmul2  9036  ledivmul2  9038  ltrec  9041  suprleubex  9112  nnle1eq1  9145  avgle1  9363  avgle2  9364  nn0le0eq0  9408  znnnlt1  9505  zleltp1  9513  elz2  9529  uzm1  9765  uzin  9767  difrp  9900  xrletri3  10012  xgepnf  10024  xltnegi  10043  xltadd1  10084  xposdif  10090  xleaddadd  10095  elioo5  10141  elfz5  10225  fzdifsuc  10289  elfzm11  10299  uzsplit  10300  elfzonelfzo  10448  qtri3or  10472  qavgle  10490  flqbi  10522  flqbi2  10523  fldiv4lem1div2uz2  10538  zmodid2  10586  q2submod  10619  sqap0  10840  lt2sq  10847  le2sq  10848  nn0opthlem1d  10954  bcval5  10997  zfz1isolemiso  11074  pfxsuffeqwrdeq  11245  shftfib  11349  mulreap  11390  caucvgrelemcau  11506  caucvgre  11507  elicc4abs  11620  abs2difabs  11634  cau4  11642  maxclpr  11748  negfi  11754  lemininf  11760  mul0inf  11767  xrlemininf  11797  xrminltinf  11798  clim2  11809  climeq  11825  fisumss  11918  fsumabs  11991  isumshft  12016  absefib  12297  dvdsval3  12317  dvdslelemd  12369  dvdsabseq  12373  dvdsflip  12377  dvdsssfz1  12378  zeo3  12394  ndvdsadd  12457  bitscmp  12484  dvdssq  12567  algcvgblem  12586  lcmdvds  12616  ncoprmgcdgt1b  12627  isprm3  12655  phiprmpw  12759  prmdiv  12772  pc11  12869  pcz  12870  pockthlem  12894  1arith  12905  ercpbllemg  13378  grpinvcnv  13616  eqger  13776  ablsubadd  13864  dvdsr02  14084  opprunitd  14089  unitsubm  14098  issubrg3  14226  aprval  14261  rnglidlmmgm  14475  znleval2  14633  discld  14825  isneip  14835  restopnb  14870  restopn2  14872  restdis  14873  lmbr2  14903  cnptoprest  14928  cnptoprest2  14929  tx1cn  14958  tx2cn  14959  txcnmpt  14962  txrest  14965  elbl2ps  15081  elbl2  15082  blcomps  15085  blcom  15086  xblpnfps  15087  xblpnf  15088  blpnf  15089  xmeter  15125  bdxmet  15190  metrest  15195  xmetxp  15196  metcn  15203  cncfcdm  15271  reefiso  15466  gausslemma2dlem0c  15745  lgseisenlem3  15766  lgsquadlem1  15771  m1lgs  15779  2lgsoddprmlem2  15800  ausgrusgrben  15981