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  883  3anibar  1150  xor2dc  1372  bilukdc  1378  reuhypd  4429  opelresi  4874  iota1  5146  funbrfv2b  5510  dffn5im  5511  fneqeql  5572  f1ompt  5615  dff13  5713  fliftcnv  5740  isotr  5761  isoini  5763  caovord3  5988  releldm2  6127  tpostpos  6205  nnsssuc  6442  nnaordi  6448  iserd  6499  ecdmn0m  6515  qliftel  6553  qliftfun  6555  qliftf  6558  ecopovsym  6569  mapen  6784  supisolem  6944  cnvti  6955  omp1eomlem  7028  ctssdc  7047  isomnimap  7063  ismkvmap  7080  iswomnimap  7092  recmulnqg  7294  nqtri3or  7299  ltmnqg  7304  mullocprlem  7473  addextpr  7524  gt0srpr  7651  ltsosr  7667  ltasrg  7673  map2psrprg  7708  xrlenlt  7925  letri3  7941  subadd  8061  ltsubadd2  8291  lesubadd2  8293  suble  8298  ltsub23  8300  ltaddpos2  8311  ltsubpos  8312  subge02  8336  ltaddsublt  8429  reapneg  8455  apsym  8464  apti  8480  leltap  8483  ap0gt0  8498  divmulap  8531  divmulap3  8533  rec11rap  8567  ltdiv1  8722  ltdivmul2  8732  ledivmul2  8734  ltrec  8737  suprleubex  8808  nnle1eq1  8840  avgle1  9056  avgle2  9057  nn0le0eq0  9101  znnnlt1  9198  zleltp1  9205  elz2  9218  uzm1  9452  uzin  9454  difrp  9581  xrletri3  9691  xgepnf  9702  xltnegi  9721  xltadd1  9762  xposdif  9768  xleaddadd  9773  elioo5  9819  elfz5  9902  fzdifsuc  9965  elfzm11  9975  uzsplit  9976  elfzonelfzo  10111  qtri3or  10124  qavgle  10140  flqbi  10171  flqbi2  10172  zmodid2  10233  q2submod  10266  sqap0  10467  lt2sq  10474  le2sq  10475  nn0opthlem1d  10576  bcval5  10619  zfz1isolemiso  10692  shftfib  10705  mulreap  10746  caucvgrelemcau  10862  caucvgre  10863  elicc4abs  10976  abs2difabs  10990  cau4  10998  maxclpr  11104  negfi  11109  lemininf  11115  mul0inf  11122  xrlemininf  11150  xrminltinf  11151  clim2  11162  climeq  11178  fisumss  11271  fsumabs  11344  isumshft  11369  absefib  11649  dvdsval3  11669  dvdslelemd  11716  dvdsabseq  11720  dvdsflip  11724  dvdsssfz1  11725  zeo3  11740  ndvdsadd  11803  dvdssq  11895  algcvgblem  11906  lcmdvds  11936  ncoprmgcdgt1b  11947  isprm3  11975  phiprmpw  12074  prmdiv  12087  discld  12496  isneip  12506  restopnb  12541  restopn2  12543  restdis  12544  lmbr2  12574  cnptoprest  12599  cnptoprest2  12600  tx1cn  12629  tx2cn  12630  txcnmpt  12633  txrest  12636  elbl2ps  12752  elbl2  12753  blcomps  12756  blcom  12757  xblpnfps  12758  xblpnf  12759  blpnf  12760  xmeter  12796  bdxmet  12861  metrest  12866  xmetxp  12867  metcn  12874  cncffvrn  12929  reefiso  13058