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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitr2d  216  3bitr2rd  217  3bitr4d  220  3bitr4rd  221  mpbirand  445  mpbiran2d  446  bianabs  619  imordc  909  ifpnst  1001  3anibar  1196  xor2dc  1439  bilukdc  1445  snelpwg  4350  prelpw  4353  reuhypd  4617  opelresi  5074  iota1  5352  funbrfv2b  5747  dffn5im  5748  fneqeql  5817  f1ompt  5859  dff13  5974  fliftcnv  6001  isotr  6022  isoini  6024  caovord3  6263  releldm2  6419  tpostpos  6535  nnsssuc  6775  nnaordi  6781  iserd  6833  ecdmn0m  6851  qliftel  6889  qliftfun  6891  qliftf  6894  ecopovsym  6905  pw2f1odclem  7134  mapen  7146  suppeqfsuppbi  7295  supisolem  7349  cnvti  7360  omp1eomlem  7435  ctssdc  7454  isomnimap  7478  ismkvmap  7495  iswomnimap  7507  netap  7621  2omotaplemap  7624  recmulnqg  7759  nqtri3or  7764  ltmnqg  7769  mullocprlem  7938  addextpr  7989  gt0srpr  8116  ltsosr  8132  ltasrg  8138  map2psrprg  8173  xrlenlt  8391  letri3  8407  subadd  8531  ltsubadd2  8763  lesubadd2  8765  suble  8770  ltsub23  8772  ltaddpos2  8783  ltsubpos  8784  subge02  8808  ltaddsublt  8902  reapneg  8928  apsym  8937  apti  8953  leltap  8956  ap0gt0  8971  divmulap  9008  divmulap3  9010  rec11rap  9044  ltdiv1  9201  ltdivmul2  9211  ledivmul2  9213  ltrec  9216  suprleubex  9287  nnle1eq1  9331  avgle1  9551  avgle2  9552  nn0le0eq0  9596  znnnlt1  9697  zleltp1  9705  elz2  9721  uzm1  9963  uzin  9965  difrp  10104  xrletri3  10217  xgepnf  10229  xltnegi  10248  xltadd1  10289  xposdif  10295  xleaddadd  10300  elioo5  10346  elfz5  10431  fzdifsuc  10499  elfzm11  10509  uzsplit  10510  elfzonelfzo  10659  qtri3or  10686  qavgle  10704  flqbi  10740  flqbi2  10741  fldiv4lem1div2uz2  10756  zmodid2  10804  q2submod  10837  sqap0  11058  lt2sq  11065  le2sq  11066  nn0opthlem1d  11174  bcval5  11217  zfz1isolemiso  11307  pfxsuffeqwrdeq  11486  shftfib  11604  mulreap  11645  caucvgrelemcau  11762  caucvgre  11763  elicc4abs  11877  abs2difabs  11891  cau4  11899  maxclpr  12005  negfi  12011  lemininf  12018  mul0inf  12026  xrlemininf  12056  xrminltinf  12057  clim2  12068  climeq  12084  fisumss  12178  fsumabs  12251  isumshft  12276  absefib  12557  dvdsval3  12577  dvdslelemd  12629  dvdsabseq  12633  dvdsflip  12637  dvdsssfz1  12638  zeo3  12654  ndvdsadd  12717  bitscmp  12744  dvdssq  12827  algcvgblem  12846  lcmdvds  12876  ncoprmgcdgt1b  12887  isprm3  12915  phiprmpw  13023  prmdiv  13036  pc11  13133  pcz  13134  pockthlem  13158  1arith  13169  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemodife  13292  ballotfilemsima  13311  ballotfilemfrcn0  13325  ercpbllemg  13704  grpinvcnv  13926  eqger  14080  ablsubadd  14200  dvdsr02  14496  opprunitd  14501  unitsubm  14510  issubrg3  14639  aprval  14675  opprdrng  14704  rnglidlmmgm  14917  znleval2  15073  discld  15328  isneip  15338  restopnb  15373  restopn2  15375  restdis  15376  lmbr2  15406  cnptoprest  15431  cnptoprest2  15432  tx1cn  15461  tx2cn  15462  txcnmpt  15465  txrest  15468  elbl2ps  15584  elbl2  15585  blcomps  15588  blcom  15589  xblpnfps  15590  xblpnf  15591  blpnf  15592  xmeter  15628  bdxmet  15693  metrest  15698  xmetxp  15699  metcn  15706  cncfcdm  15774  reefiso  15969  bclbnd  16268  bposlem1  16272  bposlem5  16276  bpos  16281  gausslemma2dlem0c  16336  lgseisenlem3  16357  lgsquadlem1  16362  m1lgs  16370  2lgsoddprmlem2  16391  ausgrusgrben  16575  eupth2lemsfi  16885