Theorem bitr4d 190

Description: Deduction form of bitr4i 186. (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 140	. 2 |- ( ph -> ( ch <-> th ) )
4	1, 3	bitrd 187	1 |- ( ph -> ( ps <-> th ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitr2d  215  3bitr2rd  216  3bitr4d  219  3bitr4rd  220  mpbirand  439  mpbiran2d  440  bianabs  606  imordc  892  3anibar  1160  xor2dc  1385  bilukdc  1391  reuhypd  4456  opelresi  4902  iota1  5174  funbrfv2b  5541  dffn5im  5542  fneqeql  5604  f1ompt  5647  dff13  5747  fliftcnv  5774  isotr  5795  isoini  5797  caovord3  6026  releldm2  6164  tpostpos  6243  nnsssuc  6481  nnaordi  6487  iserd  6539  ecdmn0m  6555  qliftel  6593  qliftfun  6595  qliftf  6598  ecopovsym  6609  mapen  6824  supisolem  6985  cnvti  6996  omp1eomlem  7071  ctssdc  7090  isomnimap  7113  ismkvmap  7130  iswomnimap  7142  recmulnqg  7353  nqtri3or  7358  ltmnqg  7363  mullocprlem  7532  addextpr  7583  gt0srpr  7710  ltsosr  7726  ltasrg  7732  map2psrprg  7767  xrlenlt  7984  letri3  8000  subadd  8122  ltsubadd2  8352  lesubadd2  8354  suble  8359  ltsub23  8361  ltaddpos2  8372  ltsubpos  8373  subge02  8397  ltaddsublt  8490  reapneg  8516  apsym  8525  apti  8541  leltap  8544  ap0gt0  8559  divmulap  8592  divmulap3  8594  rec11rap  8628  ltdiv1  8784  ltdivmul2  8794  ledivmul2  8796  ltrec  8799  suprleubex  8870  nnle1eq1  8902  avgle1  9118  avgle2  9119  nn0le0eq0  9163  znnnlt1  9260  zleltp1  9267  elz2  9283  uzm1  9517  uzin  9519  difrp  9649  xrletri3  9761  xgepnf  9773  xltnegi  9792  xltadd1  9833  xposdif  9839  xleaddadd  9844  elioo5  9890  elfz5  9973  fzdifsuc  10037  elfzm11  10047  uzsplit  10048  elfzonelfzo  10186  qtri3or  10199  qavgle  10215  flqbi  10246  flqbi2  10247  zmodid2  10308  q2submod  10341  sqap0  10542  lt2sq  10549  le2sq  10550  nn0opthlem1d  10654  bcval5  10697  zfz1isolemiso  10774  shftfib  10787  mulreap  10828  caucvgrelemcau  10944  caucvgre  10945  elicc4abs  11058  abs2difabs  11072  cau4  11080  maxclpr  11186  negfi  11191  lemininf  11197  mul0inf  11204  xrlemininf  11234  xrminltinf  11235  clim2  11246  climeq  11262  fisumss  11355  fsumabs  11428  isumshft  11453  absefib  11733  dvdsval3  11753  dvdslelemd  11803  dvdsabseq  11807  dvdsflip  11811  dvdsssfz1  11812  zeo3  11827  ndvdsadd  11890  dvdssq  11986  algcvgblem  12003  lcmdvds  12033  ncoprmgcdgt1b  12044  isprm3  12072  phiprmpw  12176  prmdiv  12189  pc11  12284  pcz  12285  pockthlem  12308  1arith  12319  grpinvcnv  12767  discld  12930  isneip  12940  restopnb  12975  restopn2  12977  restdis  12978  lmbr2  13008  cnptoprest  13033  cnptoprest2  13034  tx1cn  13063  tx2cn  13064  txcnmpt  13067  txrest  13070  elbl2ps  13186  elbl2  13187  blcomps  13190  blcom  13191  xblpnfps  13192  xblpnf  13193  blpnf  13194  xmeter  13230  bdxmet  13295  metrest  13300  xmetxp  13301  metcn  13308  cncffvrn  13363  reefiso  13492