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  615  imordc  905  ifpnst  997  3anibar  1192  xor2dc  1435  bilukdc  1441  snelpwg  4326  prelpw  4329  reuhypd  4592  opelresi  5049  iota1  5327  funbrfv2b  5721  dffn5im  5722  fneqeql  5786  f1ompt  5828  dff13  5941  fliftcnv  5968  isotr  5989  isoini  5991  caovord3  6228  releldm2  6379  tpostpos  6495  nnsssuc  6735  nnaordi  6741  iserd  6793  ecdmn0m  6811  qliftel  6849  qliftfun  6851  qliftf  6854  ecopovsym  6865  pw2f1odclem  7087  mapen  7099  suppeqfsuppbi  7248  supisolem  7299  cnvti  7310  omp1eomlem  7385  ctssdc  7404  isomnimap  7428  ismkvmap  7445  iswomnimap  7457  netap  7568  2omotaplemap  7571  recmulnqg  7706  nqtri3or  7711  ltmnqg  7716  mullocprlem  7885  addextpr  7936  gt0srpr  8063  ltsosr  8079  ltasrg  8085  map2psrprg  8120  xrlenlt  8338  letri3  8354  subadd  8476  ltsubadd2  8707  lesubadd2  8709  suble  8714  ltsub23  8716  ltaddpos2  8727  ltsubpos  8728  subge02  8752  ltaddsublt  8845  reapneg  8871  apsym  8880  apti  8896  leltap  8899  ap0gt0  8914  divmulap  8949  divmulap3  8951  rec11rap  8985  ltdiv1  9142  ltdivmul2  9152  ledivmul2  9154  ltrec  9157  suprleubex  9228  nnle1eq1  9261  avgle1  9479  avgle2  9480  nn0le0eq0  9524  znnnlt1  9625  zleltp1  9633  elz2  9649  uzm1  9885  uzin  9887  difrp  10025  xrletri3  10137  xgepnf  10149  xltnegi  10168  xltadd1  10209  xposdif  10215  xleaddadd  10220  elioo5  10266  elfz5  10351  fzdifsuc  10415  elfzm11  10425  uzsplit  10426  elfzonelfzo  10575  qtri3or  10600  qavgle  10618  flqbi  10650  flqbi2  10651  fldiv4lem1div2uz2  10666  zmodid2  10714  q2submod  10747  sqap0  10968  lt2sq  10975  le2sq  10976  nn0opthlem1d  11082  bcval5  11125  zfz1isolemiso  11211  pfxsuffeqwrdeq  11390  shftfib  11508  mulreap  11549  caucvgrelemcau  11665  caucvgre  11666  elicc4abs  11779  abs2difabs  11793  cau4  11801  maxclpr  11907  negfi  11913  lemininf  11919  mul0inf  11926  xrlemininf  11956  xrminltinf  11957  clim2  11968  climeq  11984  fisumss  12078  fsumabs  12151  isumshft  12176  absefib  12457  dvdsval3  12477  dvdslelemd  12529  dvdsabseq  12533  dvdsflip  12537  dvdsssfz1  12538  zeo3  12554  ndvdsadd  12617  bitscmp  12644  dvdssq  12727  algcvgblem  12746  lcmdvds  12776  ncoprmgcdgt1b  12787  isprm3  12815  phiprmpw  12919  prmdiv  12932  pc11  13029  pcz  13030  pockthlem  13054  1arith  13065  ercpbllemg  13543  grpinvcnv  13781  eqger  13941  ablsubadd  14029  dvdsr02  14250  opprunitd  14255  unitsubm  14264  issubrg3  14392  aprval  14428  rnglidlmmgm  14644  znleval2  14802  discld  15001  isneip  15011  restopnb  15046  restopn2  15048  restdis  15049  lmbr2  15079  cnptoprest  15104  cnptoprest2  15105  tx1cn  15134  tx2cn  15135  txcnmpt  15138  txrest  15141  elbl2ps  15257  elbl2  15258  blcomps  15261  blcom  15262  xblpnfps  15263  xblpnf  15264  blpnf  15265  xmeter  15301  bdxmet  15366  metrest  15371  xmetxp  15372  metcn  15379  cncfcdm  15447  reefiso  15642  gausslemma2dlem0c  15924  lgseisenlem3  15945  lgsquadlem1  15950  m1lgs  15958  2lgsoddprmlem2  15979  ausgrusgrben  16163  eupth2lemsfi  16473