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  4350  prelpw  4353  reuhypd  4617  opelresi  5074  iota1  5352  funbrfv2b  5747  dffn5im  5748  fneqeql  5817  f1ompt  5859  dff13  5974  fliftcnv  6001  isotr  6022  isoini  6024  caovord3  6263  releldm2  6419  tpostpos  6535  nnsssuc  6775  nnaordi  6781  iserd  6833  ecdmn0m  6851  qliftel  6889  qliftfun  6891  qliftf  6894  ecopovsym  6905  pw2f1odclem  7134  mapen  7146  suppeqfsuppbi  7295  supisolem  7348  cnvti  7359  omp1eomlem  7434  ctssdc  7453  isomnimap  7477  ismkvmap  7494  iswomnimap  7506  netap  7620  2omotaplemap  7623  recmulnqg  7758  nqtri3or  7763  ltmnqg  7768  mullocprlem  7937  addextpr  7988  gt0srpr  8115  ltsosr  8131  ltasrg  8137  map2psrprg  8172  xrlenlt  8390  letri3  8406  subadd  8530  ltsubadd2  8762  lesubadd2  8764  suble  8769  ltsub23  8771  ltaddpos2  8782  ltsubpos  8783  subge02  8807  ltaddsublt  8901  reapneg  8927  apsym  8936  apti  8952  leltap  8955  ap0gt0  8970  divmulap  9007  divmulap3  9009  rec11rap  9043  ltdiv1  9200  ltdivmul2  9210  ledivmul2  9212  ltrec  9215  suprleubex  9286  nnle1eq1  9330  avgle1  9550  avgle2  9551  nn0le0eq0  9595  znnnlt1  9696  zleltp1  9704  elz2  9720  uzm1  9962  uzin  9964  difrp  10103  xrletri3  10216  xgepnf  10228  xltnegi  10247  xltadd1  10288  xposdif  10294  xleaddadd  10299  elioo5  10345  elfz5  10430  fzdifsuc  10498  elfzm11  10508  uzsplit  10509  elfzonelfzo  10658  qtri3or  10685  qavgle  10703  flqbi  10738  flqbi2  10739  fldiv4lem1div2uz2  10754  zmodid2  10802  q2submod  10835  sqap0  11056  lt2sq  11063  le2sq  11064  nn0opthlem1d  11172  bcval5  11215  zfz1isolemiso  11305  pfxsuffeqwrdeq  11484  shftfib  11602  mulreap  11643  caucvgrelemcau  11760  caucvgre  11761  elicc4abs  11875  abs2difabs  11889  cau4  11897  maxclpr  12003  negfi  12009  lemininf  12015  mul0inf  12023  xrlemininf  12053  xrminltinf  12054  clim2  12065  climeq  12081  fisumss  12175  fsumabs  12248  isumshft  12273  absefib  12554  dvdsval3  12574  dvdslelemd  12626  dvdsabseq  12630  dvdsflip  12634  dvdsssfz1  12635  zeo3  12651  ndvdsadd  12714  bitscmp  12741  dvdssq  12824  algcvgblem  12843  lcmdvds  12873  ncoprmgcdgt1b  12884  isprm3  12912  phiprmpw  13020  prmdiv  13033  pc11  13130  pcz  13131  pockthlem  13155  1arith  13166  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemodife  13289  ballotfilemsima  13308  ballotfilemfrcn0  13322  ercpbllemg  13700  grpinvcnv  13922  eqger  14076  ablsubadd  14165  dvdsr02  14461  opprunitd  14466  unitsubm  14475  issubrg3  14604  aprval  14640  opprdrng  14669  rnglidlmmgm  14882  znleval2  15038  discld  15286  isneip  15296  restopnb  15331  restopn2  15333  restdis  15334  lmbr2  15364  cnptoprest  15389  cnptoprest2  15390  tx1cn  15419  tx2cn  15420  txcnmpt  15423  txrest  15426  elbl2ps  15542  elbl2  15543  blcomps  15546  blcom  15547  xblpnfps  15548  xblpnf  15549  blpnf  15550  xmeter  15586  bdxmet  15651  metrest  15656  xmetxp  15657  metcn  15664  cncfcdm  15732  reefiso  15927  bclbnd  16205  bposlem1  16209  bposlem5  16213  gausslemma2dlem0c  16268  lgseisenlem3  16289  lgsquadlem1  16294  m1lgs  16302  2lgsoddprmlem2  16323  ausgrusgrben  16507  eupth2lemsfi  16817