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  611  imordc  897  3anibar  1165  xor2dc  1390  bilukdc  1396  reuhypd  4472  opelresi  4919  iota1  5193  funbrfv2b  5561  dffn5im  5562  fneqeql  5625  f1ompt  5668  dff13  5769  fliftcnv  5796  isotr  5817  isoini  5819  caovord3  6048  releldm2  6186  tpostpos  6265  nnsssuc  6503  nnaordi  6509  iserd  6561  ecdmn0m  6577  qliftel  6615  qliftfun  6617  qliftf  6620  ecopovsym  6631  mapen  6846  supisolem  7007  cnvti  7018  omp1eomlem  7093  ctssdc  7112  isomnimap  7135  ismkvmap  7152  iswomnimap  7164  netap  7253  2omotaplemap  7256  recmulnqg  7390  nqtri3or  7395  ltmnqg  7400  mullocprlem  7569  addextpr  7620  gt0srpr  7747  ltsosr  7763  ltasrg  7769  map2psrprg  7804  xrlenlt  8022  letri3  8038  subadd  8160  ltsubadd2  8390  lesubadd2  8392  suble  8397  ltsub23  8399  ltaddpos2  8410  ltsubpos  8411  subge02  8435  ltaddsublt  8528  reapneg  8554  apsym  8563  apti  8579  leltap  8582  ap0gt0  8597  divmulap  8632  divmulap3  8634  rec11rap  8668  ltdiv1  8825  ltdivmul2  8835  ledivmul2  8837  ltrec  8840  suprleubex  8911  nnle1eq1  8943  avgle1  9159  avgle2  9160  nn0le0eq0  9204  znnnlt1  9301  zleltp1  9308  elz2  9324  uzm1  9558  uzin  9560  difrp  9692  xrletri3  9804  xgepnf  9816  xltnegi  9835  xltadd1  9876  xposdif  9882  xleaddadd  9887  elioo5  9933  elfz5  10017  fzdifsuc  10081  elfzm11  10091  uzsplit  10092  elfzonelfzo  10230  qtri3or  10243  qavgle  10259  flqbi  10290  flqbi2  10291  zmodid2  10352  q2submod  10385  sqap0  10587  lt2sq  10594  le2sq  10595  nn0opthlem1d  10700  bcval5  10743  zfz1isolemiso  10819  shftfib  10832  mulreap  10873  caucvgrelemcau  10989  caucvgre  10990  elicc4abs  11103  abs2difabs  11117  cau4  11125  maxclpr  11231  negfi  11236  lemininf  11242  mul0inf  11249  xrlemininf  11279  xrminltinf  11280  clim2  11291  climeq  11307  fisumss  11400  fsumabs  11473  isumshft  11498  absefib  11778  dvdsval3  11798  dvdslelemd  11849  dvdsabseq  11853  dvdsflip  11857  dvdsssfz1  11858  zeo3  11873  ndvdsadd  11936  dvdssq  12032  algcvgblem  12049  lcmdvds  12079  ncoprmgcdgt1b  12090  isprm3  12118  phiprmpw  12222  prmdiv  12235  pc11  12330  pcz  12331  pockthlem  12354  1arith  12365  ercpbllemg  12749  grpinvcnv  12938  eqger  13083  ablsubadd  13115  dvdsr02  13274  opprunitd  13279  unitsubm  13288  issubrg3  13368  aprval  13372  discld  13639  isneip  13649  restopnb  13684  restopn2  13686  restdis  13687  lmbr2  13717  cnptoprest  13742  cnptoprest2  13743  tx1cn  13772  tx2cn  13773  txcnmpt  13776  txrest  13779  elbl2ps  13895  elbl2  13896  blcomps  13899  blcom  13900  xblpnfps  13901  xblpnf  13902  blpnf  13903  xmeter  13939  bdxmet  14004  metrest  14009  xmetxp  14010  metcn  14017  cncfcdm  14072  reefiso  14201  m1lgs  14455  2lgsoddprmlem2  14457