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  615  imordc  905  ifpnst  997  3anibar  1192  xor2dc  1435  bilukdc  1441  snelpwg  4331  prelpw  4334  reuhypd  4597  opelresi  5054  iota1  5332  funbrfv2b  5726  dffn5im  5727  fneqeql  5791  f1ompt  5833  dff13  5947  fliftcnv  5974  isotr  5995  isoini  5997  caovord3  6236  releldm2  6392  tpostpos  6508  nnsssuc  6748  nnaordi  6754  iserd  6806  ecdmn0m  6824  qliftel  6862  qliftfun  6864  qliftf  6867  ecopovsym  6878  pw2f1odclem  7100  mapen  7112  suppeqfsuppbi  7261  supisolem  7312  cnvti  7323  omp1eomlem  7398  ctssdc  7417  isomnimap  7441  ismkvmap  7458  iswomnimap  7470  netap  7584  2omotaplemap  7587  recmulnqg  7722  nqtri3or  7727  ltmnqg  7732  mullocprlem  7901  addextpr  7952  gt0srpr  8079  ltsosr  8095  ltasrg  8101  map2psrprg  8136  xrlenlt  8354  letri3  8370  subadd  8492  ltsubadd2  8724  lesubadd2  8726  suble  8731  ltsub23  8733  ltaddpos2  8744  ltsubpos  8745  subge02  8769  ltaddsublt  8862  reapneg  8888  apsym  8897  apti  8913  leltap  8916  ap0gt0  8931  divmulap  8966  divmulap3  8968  rec11rap  9002  ltdiv1  9159  ltdivmul2  9169  ledivmul2  9171  ltrec  9174  suprleubex  9245  nnle1eq1  9278  avgle1  9496  avgle2  9497  nn0le0eq0  9541  znnnlt1  9642  zleltp1  9650  elz2  9666  uzm1  9903  uzin  9905  difrp  10043  xrletri3  10156  xgepnf  10168  xltnegi  10187  xltadd1  10228  xposdif  10234  xleaddadd  10239  elioo5  10285  elfz5  10370  fzdifsuc  10437  elfzm11  10447  uzsplit  10448  elfzonelfzo  10597  qtri3or  10624  qavgle  10642  flqbi  10674  flqbi2  10675  fldiv4lem1div2uz2  10690  zmodid2  10738  q2submod  10771  sqap0  10992  lt2sq  10999  le2sq  11000  nn0opthlem1d  11107  bcval5  11150  zfz1isolemiso  11236  pfxsuffeqwrdeq  11415  shftfib  11533  mulreap  11574  caucvgrelemcau  11690  caucvgre  11691  elicc4abs  11804  abs2difabs  11818  cau4  11826  maxclpr  11932  negfi  11938  lemininf  11944  mul0inf  11951  xrlemininf  11981  xrminltinf  11982  clim2  11993  climeq  12009  fisumss  12103  fsumabs  12176  isumshft  12201  absefib  12482  dvdsval3  12502  dvdslelemd  12554  dvdsabseq  12558  dvdsflip  12562  dvdsssfz1  12563  zeo3  12579  ndvdsadd  12642  bitscmp  12669  dvdssq  12752  algcvgblem  12771  lcmdvds  12801  ncoprmgcdgt1b  12812  isprm3  12840  phiprmpw  12944  prmdiv  12957  pc11  13054  pcz  13055  pockthlem  13079  1arith  13090  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemodife  13184  ballotfilemsima  13203  ballotfilemfrcn0  13217  ercpbllemg  13594  grpinvcnv  13823  eqger  13977  ablsubadd  14065  dvdsr02  14350  opprunitd  14355  unitsubm  14364  issubrg3  14493  aprval  14529  opprdrng  14558  rnglidlmmgm  14770  znleval2  14928  discld  15127  isneip  15137  restopnb  15172  restopn2  15174  restdis  15175  lmbr2  15205  cnptoprest  15230  cnptoprest2  15231  tx1cn  15260  tx2cn  15261  txcnmpt  15264  txrest  15267  elbl2ps  15383  elbl2  15384  blcomps  15387  blcom  15388  xblpnfps  15389  xblpnf  15390  blpnf  15391  xmeter  15427  bdxmet  15492  metrest  15497  xmetxp  15498  metcn  15505  cncfcdm  15573  reefiso  15768  gausslemma2dlem0c  16050  lgseisenlem3  16071  lgsquadlem1  16076  m1lgs  16084  2lgsoddprmlem2  16105  ausgrusgrben  16289  eupth2lemsfi  16599