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-1 5  ax-2 6  ax-mp 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  bianabs  579  imordc  837  3anibar  1114  xor2dc  1333  bilukdc  1339  reuhypd  4321  opelresi  4756  iota1  5028  funbrfv2b  5384  dffn5im  5385  fneqeql  5446  f1ompt  5489  dff13  5585  fliftcnv  5612  isotr  5633  isoini  5635  caovord3  5856  releldm2  5993  tpostpos  6067  nnaordi  6307  iserd  6358  ecdmn0m  6374  qliftel  6412  qliftfun  6414  qliftf  6417  ecopovsym  6428  mapen  6642  supisolem  6783  cnvti  6794  isomnimap  6880  ismkvmap  6898  recmulnqg  7047  nqtri3or  7052  ltmnqg  7057  mullocprlem  7226  addextpr  7277  gt0srpr  7391  ltsosr  7407  ltasrg  7413  xrlenlt  7648  letri3  7663  subadd  7782  ltsubadd2  8008  lesubadd2  8010  suble  8015  ltsub23  8017  ltaddpos2  8028  ltsubpos  8029  subge02  8053  ltaddsublt  8145  reapneg  8171  apsym  8180  apti  8196  leltap  8198  ap0gt0  8212  divmulap  8239  divmulap3  8241  rec11rap  8275  ltdiv1  8426  ltdivmul2  8436  ledivmul2  8438  ltrec  8441  suprleubex  8512  nnle1eq1  8544  avgle1  8754  avgle2  8755  nn0le0eq0  8799  znnnlt1  8896  zleltp1  8903  elz2  8916  uzm1  9148  uzin  9150  difrp  9269  xrletri3  9371  xgepnf  9382  xltnegi  9401  xltadd1  9442  xposdif  9448  xleaddadd  9453  elioo5  9499  elfz5  9581  fzdifsuc  9644  elfzm11  9654  uzsplit  9655  elfzonelfzo  9790  qtri3or  9803  qavgle  9819  flqbi  9846  flqbi2  9847  zmodid2  9908  q2submod  9941  sqap0  10136  lt2sq  10143  le2sq  10144  nn0opthlem1d  10243  bcval5  10286  zfz1isolemiso  10359  shftfib  10372  mulreap  10413  caucvgrelemcau  10528  caucvgre  10529  elicc4abs  10642  abs2difabs  10656  cau4  10664  maxclpr  10770  negfi  10774  lemininf  10780  xrlemininf  10814  xrminltinf  10815  clim2  10826  climeq  10842  fisumss  10935  fsumabs  11008  isumshft  11033  absefib  11209  dvdsval3  11227  dvdslelemd  11271  dvdsabseq  11275  dvdsflip  11279  dvdsssfz1  11280  zeo3  11295  ndvdsadd  11358  dvdssq  11447  algcvgblem  11458  lcmdvds  11488  ncoprmgcdgt1b  11499  isprm3  11527  phiprmpw  11625  discld  11988  isneip  11998  restopnb  12033  restopn2  12035  restdis  12036  lmbr2  12065  cnptoprest  12090  cnptoprest2  12091  elbl2ps  12178  elbl2  12179  blcomps  12182  blcom  12183  xblpnfps  12184  xblpnf  12185  blpnf  12186  xmeter  12222  bdxmet  12287  metrest  12292  metcn  12296  cncffvrn  12335