Theorem bitr4d 190

Description: Deduction form of bitr4i 186. (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 140	. 2 |- ( ph -> ( ch <-> th ) )
4	1, 3	bitrd 187	1 |- ( ph -> ( ps <-> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitr2d  215  3bitr2rd  216  3bitr4d  219  3bitr4rd  220  mpbirand  438  mpbiran2d  439  bianabs  601  imordc  887  3anibar  1155  xor2dc  1380  bilukdc  1386  reuhypd  4449  opelresi  4895  iota1  5167  funbrfv2b  5531  dffn5im  5532  fneqeql  5593  f1ompt  5636  dff13  5736  fliftcnv  5763  isotr  5784  isoini  5786  caovord3  6015  releldm2  6153  tpostpos  6232  nnsssuc  6470  nnaordi  6476  iserd  6527  ecdmn0m  6543  qliftel  6581  qliftfun  6583  qliftf  6586  ecopovsym  6597  mapen  6812  supisolem  6973  cnvti  6984  omp1eomlem  7059  ctssdc  7078  isomnimap  7101  ismkvmap  7118  iswomnimap  7130  recmulnqg  7332  nqtri3or  7337  ltmnqg  7342  mullocprlem  7511  addextpr  7562  gt0srpr  7689  ltsosr  7705  ltasrg  7711  map2psrprg  7746  xrlenlt  7963  letri3  7979  subadd  8101  ltsubadd2  8331  lesubadd2  8333  suble  8338  ltsub23  8340  ltaddpos2  8351  ltsubpos  8352  subge02  8376  ltaddsublt  8469  reapneg  8495  apsym  8504  apti  8520  leltap  8523  ap0gt0  8538  divmulap  8571  divmulap3  8573  rec11rap  8607  ltdiv1  8763  ltdivmul2  8773  ledivmul2  8775  ltrec  8778  suprleubex  8849  nnle1eq1  8881  avgle1  9097  avgle2  9098  nn0le0eq0  9142  znnnlt1  9239  zleltp1  9246  elz2  9262  uzm1  9496  uzin  9498  difrp  9628  xrletri3  9740  xgepnf  9752  xltnegi  9771  xltadd1  9812  xposdif  9818  xleaddadd  9823  elioo5  9869  elfz5  9952  fzdifsuc  10016  elfzm11  10026  uzsplit  10027  elfzonelfzo  10165  qtri3or  10178  qavgle  10194  flqbi  10225  flqbi2  10226  zmodid2  10287  q2submod  10320  sqap0  10521  lt2sq  10528  le2sq  10529  nn0opthlem1d  10633  bcval5  10676  zfz1isolemiso  10752  shftfib  10765  mulreap  10806  caucvgrelemcau  10922  caucvgre  10923  elicc4abs  11036  abs2difabs  11050  cau4  11058  maxclpr  11164  negfi  11169  lemininf  11175  mul0inf  11182  xrlemininf  11212  xrminltinf  11213  clim2  11224  climeq  11240  fisumss  11333  fsumabs  11406  isumshft  11431  absefib  11711  dvdsval3  11731  dvdslelemd  11781  dvdsabseq  11785  dvdsflip  11789  dvdsssfz1  11790  zeo3  11805  ndvdsadd  11868  dvdssq  11964  algcvgblem  11981  lcmdvds  12011  ncoprmgcdgt1b  12022  isprm3  12050  phiprmpw  12154  prmdiv  12167  pc11  12262  pcz  12263  pockthlem  12286  1arith  12297  discld  12776  isneip  12786  restopnb  12821  restopn2  12823  restdis  12824  lmbr2  12854  cnptoprest  12879  cnptoprest2  12880  tx1cn  12909  tx2cn  12910  txcnmpt  12913  txrest  12916  elbl2ps  13032  elbl2  13033  blcomps  13036  blcom  13037  xblpnfps  13038  xblpnf  13039  blpnf  13040  xmeter  13076  bdxmet  13141  metrest  13146  xmetxp  13147  metcn  13154  cncffvrn  13209  reefiso  13338