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  611  imordc  897  3anibar  1165  xor2dc  1390  bilukdc  1396  reuhypd  4473  opelresi  4920  iota1  5194  funbrfv2b  5562  dffn5im  5563  fneqeql  5626  f1ompt  5669  dff13  5771  fliftcnv  5798  isotr  5819  isoini  5821  caovord3  6050  releldm2  6188  tpostpos  6267  nnsssuc  6505  nnaordi  6511  iserd  6563  ecdmn0m  6579  qliftel  6617  qliftfun  6619  qliftf  6622  ecopovsym  6633  mapen  6848  supisolem  7009  cnvti  7020  omp1eomlem  7095  ctssdc  7114  isomnimap  7137  ismkvmap  7154  iswomnimap  7166  netap  7255  2omotaplemap  7258  recmulnqg  7392  nqtri3or  7397  ltmnqg  7402  mullocprlem  7571  addextpr  7622  gt0srpr  7749  ltsosr  7765  ltasrg  7771  map2psrprg  7806  xrlenlt  8024  letri3  8040  subadd  8162  ltsubadd2  8392  lesubadd2  8394  suble  8399  ltsub23  8401  ltaddpos2  8412  ltsubpos  8413  subge02  8437  ltaddsublt  8530  reapneg  8556  apsym  8565  apti  8581  leltap  8584  ap0gt0  8599  divmulap  8634  divmulap3  8636  rec11rap  8670  ltdiv1  8827  ltdivmul2  8837  ledivmul2  8839  ltrec  8842  suprleubex  8913  nnle1eq1  8945  avgle1  9161  avgle2  9162  nn0le0eq0  9206  znnnlt1  9303  zleltp1  9310  elz2  9326  uzm1  9560  uzin  9562  difrp  9694  xrletri3  9806  xgepnf  9818  xltnegi  9837  xltadd1  9878  xposdif  9884  xleaddadd  9889  elioo5  9935  elfz5  10019  fzdifsuc  10083  elfzm11  10093  uzsplit  10094  elfzonelfzo  10232  qtri3or  10245  qavgle  10261  flqbi  10292  flqbi2  10293  zmodid2  10354  q2submod  10387  sqap0  10589  lt2sq  10596  le2sq  10597  nn0opthlem1d  10702  bcval5  10745  zfz1isolemiso  10821  shftfib  10834  mulreap  10875  caucvgrelemcau  10991  caucvgre  10992  elicc4abs  11105  abs2difabs  11119  cau4  11127  maxclpr  11233  negfi  11238  lemininf  11244  mul0inf  11251  xrlemininf  11281  xrminltinf  11282  clim2  11293  climeq  11309  fisumss  11402  fsumabs  11475  isumshft  11500  absefib  11780  dvdsval3  11800  dvdslelemd  11851  dvdsabseq  11855  dvdsflip  11859  dvdsssfz1  11860  zeo3  11875  ndvdsadd  11938  dvdssq  12034  algcvgblem  12051  lcmdvds  12081  ncoprmgcdgt1b  12092  isprm3  12120  phiprmpw  12224  prmdiv  12237  pc11  12332  pcz  12333  pockthlem  12356  1arith  12367  ercpbllemg  12754  grpinvcnv  12943  eqger  13088  ablsubadd  13120  dvdsr02  13279  opprunitd  13284  unitsubm  13293  issubrg3  13373  aprval  13377  discld  13721  isneip  13731  restopnb  13766  restopn2  13768  restdis  13769  lmbr2  13799  cnptoprest  13824  cnptoprest2  13825  tx1cn  13854  tx2cn  13855  txcnmpt  13858  txrest  13861  elbl2ps  13977  elbl2  13978  blcomps  13981  blcom  13982  xblpnfps  13983  xblpnf  13984  blpnf  13985  xmeter  14021  bdxmet  14086  metrest  14091  xmetxp  14092  metcn  14099  cncfcdm  14154  reefiso  14283  m1lgs  14537  2lgsoddprmlem2  14539