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  4295  prelpw  4298  reuhypd  4561  opelresi  5015  iota1  5292  funbrfv2b  5677  dffn5im  5678  fneqeql  5742  f1ompt  5785  dff13  5891  fliftcnv  5918  isotr  5939  isoini  5941  caovord3  6178  releldm2  6329  tpostpos  6408  nnsssuc  6646  nnaordi  6652  iserd  6704  ecdmn0m  6722  qliftel  6760  qliftfun  6762  qliftf  6765  ecopovsym  6776  pw2f1odclem  6991  mapen  7003  supisolem  7171  cnvti  7182  omp1eomlem  7257  ctssdc  7276  isomnimap  7300  ismkvmap  7317  iswomnimap  7329  netap  7436  2omotaplemap  7439  recmulnqg  7574  nqtri3or  7579  ltmnqg  7584  mullocprlem  7753  addextpr  7804  gt0srpr  7931  ltsosr  7947  ltasrg  7953  map2psrprg  7988  xrlenlt  8207  letri3  8223  subadd  8345  ltsubadd2  8576  lesubadd2  8578  suble  8583  ltsub23  8585  ltaddpos2  8596  ltsubpos  8597  subge02  8621  ltaddsublt  8714  reapneg  8740  apsym  8749  apti  8765  leltap  8768  ap0gt0  8783  divmulap  8818  divmulap3  8820  rec11rap  8854  ltdiv1  9011  ltdivmul2  9021  ledivmul2  9023  ltrec  9026  suprleubex  9097  nnle1eq1  9130  avgle1  9348  avgle2  9349  nn0le0eq0  9393  znnnlt1  9490  zleltp1  9498  elz2  9514  uzm1  9749  uzin  9751  difrp  9884  xrletri3  9996  xgepnf  10008  xltnegi  10027  xltadd1  10068  xposdif  10074  xleaddadd  10079  elioo5  10125  elfz5  10209  fzdifsuc  10273  elfzm11  10283  uzsplit  10284  elfzonelfzo  10431  qtri3or  10455  qavgle  10473  flqbi  10505  flqbi2  10506  fldiv4lem1div2uz2  10521  zmodid2  10569  q2submod  10602  sqap0  10823  lt2sq  10830  le2sq  10831  nn0opthlem1d  10937  bcval5  10980  zfz1isolemiso  11056  pfxsuffeqwrdeq  11225  shftfib  11329  mulreap  11370  caucvgrelemcau  11486  caucvgre  11487  elicc4abs  11600  abs2difabs  11614  cau4  11622  maxclpr  11728  negfi  11734  lemininf  11740  mul0inf  11747  xrlemininf  11777  xrminltinf  11778  clim2  11789  climeq  11805  fisumss  11898  fsumabs  11971  isumshft  11996  absefib  12277  dvdsval3  12297  dvdslelemd  12349  dvdsabseq  12353  dvdsflip  12357  dvdsssfz1  12358  zeo3  12374  ndvdsadd  12437  bitscmp  12464  dvdssq  12547  algcvgblem  12566  lcmdvds  12596  ncoprmgcdgt1b  12607  isprm3  12635  phiprmpw  12739  prmdiv  12752  pc11  12849  pcz  12850  pockthlem  12874  1arith  12885  ercpbllemg  13358  grpinvcnv  13596  eqger  13756  ablsubadd  13844  dvdsr02  14063  opprunitd  14068  unitsubm  14077  issubrg3  14205  aprval  14240  rnglidlmmgm  14454  znleval2  14612  discld  14804  isneip  14814  restopnb  14849  restopn2  14851  restdis  14852  lmbr2  14882  cnptoprest  14907  cnptoprest2  14908  tx1cn  14937  tx2cn  14938  txcnmpt  14941  txrest  14944  elbl2ps  15060  elbl2  15061  blcomps  15064  blcom  15065  xblpnfps  15066  xblpnf  15067  blpnf  15068  xmeter  15104  bdxmet  15169  metrest  15174  xmetxp  15175  metcn  15182  cncfcdm  15250  reefiso  15445  gausslemma2dlem0c  15724  lgseisenlem3  15745  lgsquadlem1  15750  m1lgs  15758  2lgsoddprmlem2  15779  ausgrusgrben  15960