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  4352  prelpw  4355  reuhypd  4619  opelresi  5076  iota1  5355  funbrfv2b  5750  dffn5im  5751  fneqeql  5820  f1ompt  5862  dff13  5977  fliftcnv  6004  isotr  6025  isoini  6027  caovord3  6266  releldm2  6423  tpostpos  6539  nnsssuc  6779  nnaordi  6785  iserd  6837  ecdmn0m  6855  qliftel  6893  qliftfun  6895  qliftf  6898  ecopovsym  6909  pw2f1odclem  7138  mapen  7150  relresfin  7268  suppeqfsuppbi  7300  supisolem  7354  cnvti  7365  omp1eomlem  7440  ctssdc  7459  isomnimap  7483  ismkvmap  7500  iswomnimap  7512  netap  7626  2omotaplemap  7629  recmulnqg  7764  nqtri3or  7769  ltmnqg  7774  mullocprlem  7943  addextpr  7994  gt0srpr  8121  ltsosr  8137  ltasrg  8143  map2psrprg  8178  xrlenlt  8396  letri3  8412  subadd  8536  ltsubadd2  8768  lesubadd2  8770  suble  8775  ltsub23  8777  ltaddpos2  8788  ltsubpos  8789  subge02  8813  ltaddsublt  8907  reapneg  8933  apsym  8942  apti  8958  leltap  8961  ap0gt0  8976  divmulap  9013  divmulap3  9015  rec11rap  9049  ltdiv1  9206  ltdivmul2  9216  ledivmul2  9218  ltrec  9221  suprleubex  9292  nnle1eq1  9337  avgle1  9557  avgle2  9558  nn0le0eq0  9602  znnnlt1  9703  zleltp1  9711  elz2  9727  uzm1  9969  uzin  9971  difrp  10110  xrletri3  10223  xgepnf  10235  xltnegi  10254  xltadd1  10295  xposdif  10301  xleaddadd  10306  elioo5  10352  elfz5  10437  fzdifsuc  10505  elfzm11  10515  uzsplit  10516  elfzonelfzo  10665  qtri3or  10692  qavgle  10710  flqbi  10746  flqbi2  10747  fldiv4lem1div2uz2  10762  zmodid2  10810  q2submod  10843  sqap0  11064  lt2sq  11071  le2sq  11072  nn0opthlem1d  11180  bcval5  11223  zfz1isolemiso  11313  pfxsuffeqwrdeq  11492  shftfib  11610  mulreap  11651  caucvgrelemcau  11768  caucvgre  11769  elicc4abs  11883  abs2difabs  11897  cau4  11905  maxclpr  12011  negfi  12017  lemininf  12024  mul0inf  12032  xrlemininf  12062  xrminltinf  12063  clim2  12074  climeq  12090  fisumss  12184  fsumabs  12257  isumshft  12282  absefib  12563  dvdsval3  12583  dvdslelemd  12635  dvdsabseq  12639  dvdsflip  12643  dvdsssfz1  12644  zeo3  12660  ndvdsadd  12723  bitscmp  12750  dvdssq  12833  algcvgblem  12852  lcmdvds  12882  ncoprmgcdgt1b  12893  isprm3  12921  phiprmpw  13029  prmdiv  13042  pc11  13139  pcz  13140  pockthlem  13164  1arith  13175  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemodife  13298  ballotfilemsima  13317  ballotfilemfrcn0  13331  ercpbllemg  13710  grpinvcnv  13932  eqger  14086  ablsubadd  14206  dvdsr02  14521  opprunitd  14526  unitsubm  14535  issubrg3  14664  aprval  14700  opprdrng  14729  rnglidlmmgm  14942  znleval2  15098  discld  15362  isneip  15372  restopnb  15407  restopn2  15409  restdis  15410  lmbr2  15440  cnptoprest  15465  cnptoprest2  15466  tx1cn  15495  tx2cn  15496  txcnmpt  15499  txrest  15502  elbl2ps  15618  elbl2  15619  blcomps  15622  blcom  15623  xblpnfps  15624  xblpnf  15625  blpnf  15626  xmeter  15662  bdxmet  15727  metrest  15732  xmetxp  15733  metcn  15740  cncfcdm  15808  reefiso  16003  bclbnd  16307  bposlem1  16311  bposlem5  16315  bpos  16320  gausslemma2dlem0c  16375  lgseisenlem3  16396  lgsquadlem1  16401  m1lgs  16409  2lgsoddprmlem2  16430  ausgrusgrben  16614  eupth2lemsfi  16924