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  suppinisegdc  6513  tpostpos  6540  nnsssuc  6780  nnaordi  6786  iserd  6838  ecdmn0m  6856  qliftel  6894  qliftfun  6896  qliftf  6899  ecopovsym  6910  pw2f1odclem  7140  mapen  7152  relresfin  7270  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  9701  zleltp1  9709  elz2  9725  uzm1  9968  uzin  9970  difrp  10109  xrletri3  10222  xgepnf  10234  xltnegi  10253  xltadd1  10294  xposdif  10300  xleaddadd  10305  elioo5  10351  elfz5  10436  fzdifsuc  10504  elfzm11  10514  uzsplit  10515  elfzonelfzo  10664  qtri3or  10691  qavgle  10709  flqbi  10745  flqbi2  10746  fldiv4lem1div2uz2  10761  zmodid2  10809  q2submod  10842  sqap0  11063  lt2sq  11070  le2sq  11071  nn0opthlem1d  11179  bcval5  11222  zfz1isolemiso  11312  pfxsuffeqwrdeq  11491  shftfib  11609  mulreap  11650  caucvgrelemcau  11767  caucvgre  11768  elicc4abs  11882  abs2difabs  11896  cau4  11904  maxclpr  12010  negfi  12016  lemininf  12023  mul0inf  12031  xrlemininf  12061  xrminltinf  12062  clim2  12073  climeq  12089  fisumss  12183  fsumabs  12256  isumshft  12281  absefib  12562  dvdsval3  12582  dvdslelemd  12634  dvdsabseq  12638  dvdsflip  12642  dvdsssfz1  12643  zeo3  12659  ndvdsadd  12722  bitscmp  12749  dvdssq  12832  algcvgblem  12851  lcmdvds  12881  ncoprmgcdgt1b  12892  isprm3  12920  phiprmpw  13028  prmdiv  13041  pc11  13138  pcz  13139  pockthlem  13163  1arith  13174  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemodife  13297  ballotfilemsima  13316  ballotfilemfrcn0  13330  ercpbllemg  13709  grpinvcnv  13931  eqger  14085  ablsubadd  14205  dvdsr02  14520  opprunitd  14525  unitsubm  14534  issubrg3  14663  aprval  14699  opprdrng  14728  rnglidlmmgm  14941  znleval2  15097  discld  15379  isneip  15389  restopnb  15424  restopn2  15426  restdis  15427  lmbr2  15457  cnptoprest  15482  cnptoprest2  15483  tx1cn  15512  tx2cn  15513  txcnmpt  15516  txrest  15519  elbl2ps  15635  elbl2  15636  blcomps  15639  blcom  15640  xblpnfps  15641  xblpnf  15642  blpnf  15643  xmeter  15679  bdxmet  15744  metrest  15749  xmetxp  15750  metcn  15757  cncfcdm  15825  reefiso  16020  bclbnd  16324  bposlem1  16328  bposlem5  16332  bpos  16337  gausslemma2dlem0c  16392  lgseisenlem3  16413  lgsquadlem1  16418  m1lgs  16426  2lgsoddprmlem2  16447  ausgrusgrben  16631  eupth2lemsfi  16941