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  445  mpbiran2d  446  bianabs  619  imordc  909  ifpnst  1001  3anibar  1196  xor2dc  1439  bilukdc  1445  snelpwg  4345  prelpw  4348  reuhypd  4612  opelresi  5069  iota1  5347  funbrfv2b  5741  dffn5im  5742  fneqeql  5808  f1ompt  5850  dff13  5964  fliftcnv  5991  isotr  6012  isoini  6014  caovord3  6253  releldm2  6409  tpostpos  6525  nnsssuc  6765  nnaordi  6771  iserd  6823  ecdmn0m  6841  qliftel  6879  qliftfun  6881  qliftf  6884  ecopovsym  6895  pw2f1odclem  7124  mapen  7136  suppeqfsuppbi  7285  supisolem  7338  cnvti  7349  omp1eomlem  7424  ctssdc  7443  isomnimap  7467  ismkvmap  7484  iswomnimap  7496  netap  7610  2omotaplemap  7613  recmulnqg  7748  nqtri3or  7753  ltmnqg  7758  mullocprlem  7927  addextpr  7978  gt0srpr  8105  ltsosr  8121  ltasrg  8127  map2psrprg  8162  xrlenlt  8380  letri3  8396  subadd  8519  ltsubadd2  8751  lesubadd2  8753  suble  8758  ltsub23  8760  ltaddpos2  8771  ltsubpos  8772  subge02  8796  ltaddsublt  8889  reapneg  8915  apsym  8924  apti  8940  leltap  8943  ap0gt0  8958  divmulap  8995  divmulap3  8997  rec11rap  9031  ltdiv1  9188  ltdivmul2  9198  ledivmul2  9200  ltrec  9203  suprleubex  9274  nnle1eq1  9307  avgle1  9525  avgle2  9526  nn0le0eq0  9570  znnnlt1  9671  zleltp1  9679  elz2  9695  uzm1  9932  uzin  9934  difrp  10072  xrletri3  10185  xgepnf  10197  xltnegi  10216  xltadd1  10257  xposdif  10263  xleaddadd  10268  elioo5  10314  elfz5  10399  fzdifsuc  10466  elfzm11  10476  uzsplit  10477  elfzonelfzo  10626  qtri3or  10653  qavgle  10671  flqbi  10703  flqbi2  10704  fldiv4lem1div2uz2  10719  zmodid2  10767  q2submod  10800  sqap0  11021  lt2sq  11028  le2sq  11029  nn0opthlem1d  11136  bcval5  11179  zfz1isolemiso  11269  pfxsuffeqwrdeq  11448  shftfib  11566  mulreap  11607  caucvgrelemcau  11724  caucvgre  11725  elicc4abs  11838  abs2difabs  11852  cau4  11860  maxclpr  11966  negfi  11972  lemininf  11978  mul0inf  11985  xrlemininf  12015  xrminltinf  12016  clim2  12027  climeq  12043  fisumss  12137  fsumabs  12210  isumshft  12235  absefib  12516  dvdsval3  12536  dvdslelemd  12588  dvdsabseq  12592  dvdsflip  12596  dvdsssfz1  12597  zeo3  12613  ndvdsadd  12676  bitscmp  12703  dvdssq  12786  algcvgblem  12805  lcmdvds  12835  ncoprmgcdgt1b  12846  isprm3  12874  phiprmpw  12978  prmdiv  12991  pc11  13088  pcz  13089  pockthlem  13113  1arith  13124  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemodife  13218  ballotfilemsima  13237  ballotfilemfrcn0  13251  ercpbllemg  13628  grpinvcnv  13850  eqger  14004  ablsubadd  14093  dvdsr02  14385  opprunitd  14390  unitsubm  14399  issubrg3  14528  aprval  14564  opprdrng  14593  rnglidlmmgm  14805  znleval2  14961  discld  15160  isneip  15170  restopnb  15205  restopn2  15207  restdis  15208  lmbr2  15238  cnptoprest  15263  cnptoprest2  15264  tx1cn  15293  tx2cn  15294  txcnmpt  15297  txrest  15300  elbl2ps  15416  elbl2  15417  blcomps  15420  blcom  15421  xblpnfps  15422  xblpnf  15423  blpnf  15424  xmeter  15460  bdxmet  15525  metrest  15530  xmetxp  15531  metcn  15538  cncfcdm  15606  reefiso  15801  gausslemma2dlem0c  16084  lgseisenlem3  16105  lgsquadlem1  16110  m1lgs  16118  2lgsoddprmlem2  16139  ausgrusgrben  16323  eupth2lemsfi  16633