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  904  ifpnst  996  3anibar  1191  xor2dc  1434  bilukdc  1440  snelpwg  4302  prelpw  4305  reuhypd  4568  opelresi  5024  iota1  5301  funbrfv2b  5690  dffn5im  5691  fneqeql  5755  f1ompt  5798  dff13  5908  fliftcnv  5935  isotr  5956  isoini  5958  caovord3  6195  releldm2  6347  tpostpos  6429  nnsssuc  6669  nnaordi  6675  iserd  6727  ecdmn0m  6745  qliftel  6783  qliftfun  6785  qliftf  6788  ecopovsym  6799  pw2f1odclem  7019  mapen  7031  supisolem  7206  cnvti  7217  omp1eomlem  7292  ctssdc  7311  isomnimap  7335  ismkvmap  7352  iswomnimap  7364  netap  7472  2omotaplemap  7475  recmulnqg  7610  nqtri3or  7615  ltmnqg  7620  mullocprlem  7789  addextpr  7840  gt0srpr  7967  ltsosr  7983  ltasrg  7989  map2psrprg  8024  xrlenlt  8243  letri3  8259  subadd  8381  ltsubadd2  8612  lesubadd2  8614  suble  8619  ltsub23  8621  ltaddpos2  8632  ltsubpos  8633  subge02  8657  ltaddsublt  8750  reapneg  8776  apsym  8785  apti  8801  leltap  8804  ap0gt0  8819  divmulap  8854  divmulap3  8856  rec11rap  8890  ltdiv1  9047  ltdivmul2  9057  ledivmul2  9059  ltrec  9062  suprleubex  9133  nnle1eq1  9166  avgle1  9384  avgle2  9385  nn0le0eq0  9429  znnnlt1  9526  zleltp1  9534  elz2  9550  uzm1  9786  uzin  9788  difrp  9926  xrletri3  10038  xgepnf  10050  xltnegi  10069  xltadd1  10110  xposdif  10116  xleaddadd  10121  elioo5  10167  elfz5  10251  fzdifsuc  10315  elfzm11  10325  uzsplit  10326  elfzonelfzo  10474  qtri3or  10499  qavgle  10517  flqbi  10549  flqbi2  10550  fldiv4lem1div2uz2  10565  zmodid2  10613  q2submod  10646  sqap0  10867  lt2sq  10874  le2sq  10875  nn0opthlem1d  10981  bcval5  11024  zfz1isolemiso  11102  pfxsuffeqwrdeq  11278  shftfib  11383  mulreap  11424  caucvgrelemcau  11540  caucvgre  11541  elicc4abs  11654  abs2difabs  11668  cau4  11676  maxclpr  11782  negfi  11788  lemininf  11794  mul0inf  11801  xrlemininf  11831  xrminltinf  11832  clim2  11843  climeq  11859  fisumss  11952  fsumabs  12025  isumshft  12050  absefib  12331  dvdsval3  12351  dvdslelemd  12403  dvdsabseq  12407  dvdsflip  12411  dvdsssfz1  12412  zeo3  12428  ndvdsadd  12491  bitscmp  12518  dvdssq  12601  algcvgblem  12620  lcmdvds  12650  ncoprmgcdgt1b  12661  isprm3  12689  phiprmpw  12793  prmdiv  12806  pc11  12903  pcz  12904  pockthlem  12928  1arith  12939  ercpbllemg  13412  grpinvcnv  13650  eqger  13810  ablsubadd  13898  dvdsr02  14118  opprunitd  14123  unitsubm  14132  issubrg3  14260  aprval  14295  rnglidlmmgm  14509  znleval2  14667  discld  14859  isneip  14869  restopnb  14904  restopn2  14906  restdis  14907  lmbr2  14937  cnptoprest  14962  cnptoprest2  14963  tx1cn  14992  tx2cn  14993  txcnmpt  14996  txrest  14999  elbl2ps  15115  elbl2  15116  blcomps  15119  blcom  15120  xblpnfps  15121  xblpnf  15122  blpnf  15123  xmeter  15159  bdxmet  15224  metrest  15229  xmetxp  15230  metcn  15237  cncfcdm  15305  reefiso  15500  gausslemma2dlem0c  15779  lgseisenlem3  15800  lgsquadlem1  15805  m1lgs  15813  2lgsoddprmlem2  15834  ausgrusgrben  16018