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  8529  ltsubadd2  8761  lesubadd2  8763  suble  8768  ltsub23  8770  ltaddpos2  8781  ltsubpos  8782  subge02  8806  ltaddsublt  8899  reapneg  8925  apsym  8934  apti  8950  leltap  8953  ap0gt0  8968  divmulap  9005  divmulap3  9007  rec11rap  9041  ltdiv1  9198  ltdivmul2  9208  ledivmul2  9210  ltrec  9213  suprleubex  9284  nnle1eq1  9328  avgle1  9546  avgle2  9547  nn0le0eq0  9591  znnnlt1  9692  zleltp1  9700  elz2  9716  uzm1  9953  uzin  9955  difrp  10093  xrletri3  10206  xgepnf  10218  xltnegi  10237  xltadd1  10278  xposdif  10284  xleaddadd  10289  elioo5  10335  elfz5  10420  fzdifsuc  10488  elfzm11  10498  uzsplit  10499  elfzonelfzo  10648  qtri3or  10675  qavgle  10693  flqbi  10725  flqbi2  10726  fldiv4lem1div2uz2  10741  zmodid2  10789  q2submod  10822  sqap0  11043  lt2sq  11050  le2sq  11051  nn0opthlem1d  11158  bcval5  11201  zfz1isolemiso  11291  pfxsuffeqwrdeq  11470  shftfib  11588  mulreap  11629  caucvgrelemcau  11746  caucvgre  11747  elicc4abs  11860  abs2difabs  11874  cau4  11882  maxclpr  11988  negfi  11994  lemininf  12000  mul0inf  12007  xrlemininf  12037  xrminltinf  12038  clim2  12049  climeq  12065  fisumss  12159  fsumabs  12232  isumshft  12257  absefib  12538  dvdsval3  12558  dvdslelemd  12610  dvdsabseq  12614  dvdsflip  12618  dvdsssfz1  12619  zeo3  12635  ndvdsadd  12698  bitscmp  12725  dvdssq  12808  algcvgblem  12827  lcmdvds  12857  ncoprmgcdgt1b  12868  isprm3  12896  phiprmpw  13000  prmdiv  13013  pc11  13110  pcz  13111  pockthlem  13135  1arith  13146  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemodife  13240  ballotfilemsima  13259  ballotfilemfrcn0  13273  ercpbllemg  13651  grpinvcnv  13873  eqger  14027  ablsubadd  14116  dvdsr02  14412  opprunitd  14417  unitsubm  14426  issubrg3  14555  aprval  14591  opprdrng  14620  rnglidlmmgm  14833  znleval2  14989  discld  15237  isneip  15247  restopnb  15282  restopn2  15284  restdis  15285  lmbr2  15315  cnptoprest  15340  cnptoprest2  15341  tx1cn  15370  tx2cn  15371  txcnmpt  15374  txrest  15377  elbl2ps  15493  elbl2  15494  blcomps  15497  blcom  15498  xblpnfps  15499  xblpnf  15500  blpnf  15501  xmeter  15537  bdxmet  15602  metrest  15607  xmetxp  15608  metcn  15615  cncfcdm  15683  reefiso  15878  gausslemma2dlem0c  16170  lgseisenlem3  16191  lgsquadlem1  16196  m1lgs  16204  2lgsoddprmlem2  16225  ausgrusgrben  16409  eupth2lemsfi  16719