Theorem bitrd 188

Description: Deduction form of bitri 184. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.)

Hypotheses

Ref	Expression
bitrd.1	|- ( ph -> ( ps <-> ch ) )
bitrd.2	|- ( ph -> ( ch <-> th ) )

Assertion

Ref	Expression
bitrd	|- ( ph -> ( ps <-> th ) )

Proof of Theorem bitrd

Step	Hyp	Ref	Expression
1		bitrd.1	. . . 4 |- ( ph -> ( ps <-> ch ) )
2	1	pm5.74i 180	. . 3 |- ( ( ph -> ps ) <-> ( ph -> ch ) )
3		bitrd.2	. . . 4 |- ( ph -> ( ch <-> th ) )
4	3	pm5.74i 180	. . 3 |- ( ( ph -> ch ) <-> ( ph -> th ) )
5	2, 4	bitri 184	. 2 |- ( ( ph -> ps ) <-> ( ph -> th ) )
6	5	pm5.74ri 181	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:  bitr2d  189  bitr3d  190  bitr4d  191  bitrid  192  bitrdi  196  3bitrd  214  3bitr2d  216  3bitr3d  218  3bitr4d  220  imbi12d  234  bibi12d  235  sylan9bb  462  anbi12d  473  orbi12d  801  con1biidc  885  pm4.54dc  910  dn1dc  969  dedlem0a  977  dfifp3dc  991  dfifp4dc  992  dfifp5dc  993  3bior2fd  1391  xorbi12d  1427  nbbndc  1439  eleq12d  2305  neeq12d  2434  neleq12d  2515  raleqbi1dv  2755  rexeqbi1dv  2756  reueqd  2757  rmoeqd  2758  raleqbidv  2759  rexeqbidv  2760  raleqbidva  2761  rexeqbidva  2762  eueq3dc  2994  sbc19.21g  3114  sbcabel  3128  sbcel1g  3160  sbceq1g  3161  sbcel2g  3162  sbceq2g  3163  sbccsb2g  3171  sbcco3g  3199  sseq12d  3273  raaanlem  3618  sbcssg  3622  ralsng  3734  2ralunsn  3908  csbunig  3927  disjeq12d  4099  breq123d  4128  sbcbr12g  4170  sbcbr1g  4171  sbcbr2g  4172  treq  4219  nalset  4245  exmidsssn  4320  copsex4g  4368  onsucb  4630  posng  4827  csbxpg  4836  sbcrel  4841  csbcnvg  4944  eliniseg  5137  brcodir  5155  csbrng  5229  sbcfung  5381  fneq12d  5453  feq12d  5503  feq123d  5504  sbcfng  5511  sbcfg  5512  f1osng  5662  csbfv12g  5715  funimass4  5732  dmfco  5750  eqfnfv  5780  eqfnfv2  5781  fneqeql2  5792  fvimacnvi  5797  funimass3  5799  fniniseg  5803  unpreima  5807  ralrnmpt  5824  rexrnmpt  5825  dffo3  5829  fmptco  5848  fressnfv  5876  eufnfv  5922  foima2  5930  fnunirn  5946  dff13  5947  f1elima  5952  cocan1  5966  cocan2  5967  fliftel  5972  fliftf  5978  isoresbr  5988  isoini  5997  f1oiso  6005  f1ofveu  6046  mpoeq123dva  6122  ovid  6178  ov  6181  ovg  6201  ovelrn  6211  caovord2d  6232  ofrfval2  6292  offveqb  6295  eqop  6384  reldm  6393  f1od2  6444  suppval1  6452  suppssrst  6474  suppssrgst  6475  mpoxopoveq  6484  mpoxopovel  6485  tpostpos  6508  smoiso  6546  frecabcl  6643  frecsuclem  6650  nnaordr  6756  nnaword  6757  nnaordex  6774  ereq1  6787  brdifun  6807  erth2  6827  qliftfun  6864  brecop  6872  elmapg  6908  elpmg  6911  mapsnd  6936  dom2lem  7024  xpcomco  7090  pw2f1odclem  7100  php5fin  7152  funisfsupp  7257  ffsuppbi  7266  elfi2  7272  supisolem  7312  inflbti  7328  inl11  7369  ismkvnex  7459  mkvprop  7462  nninfwlporlemd  7476  exmidfodomrlemreseldju  7516  ltapig  7669  ltmpig  7670  nlt1pig  7672  mulcmpblnq  7699  ltsonq  7729  lt2addnq  7735  lt2mulnq  7736  archnqq  7748  prarloclemarch  7749  ltrnqg  7751  mulcmpblnq0  7775  preqlu  7803  genpdflem  7838  addnqprllem  7858  addnqprulem  7859  addlocprlemgt  7865  appdivnq  7894  mulnqprl  7899  mulnqpru  7900  mullocprlem  7901  distrlem4prl  7915  distrlem4pru  7916  1idprl  7921  1idpru  7922  ltexprlemloc  7938  cauappcvgprlemladdrl  7988  cauappcvgprlemladd  7989  cauappcvgprlem1  7990  archrecnq  7994  caucvgprlemnkj  7997  caucvgprprlemexb  8038  addcmpblnr  8070  lttrsr  8093  ltsosr  8095  ltasrg  8101  mulextsr1  8112  srpospr  8114  caucvgsrlemcau  8124  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  map2psrprg  8136  ltresr  8170  axcaucvglemres  8230  eqlelt  8376  cnegexlem1  8465  negeu  8481  subadd2  8494  subcan2  8515  addrsub  8661  ltaddneg  8716  ltaddnegr  8717  ltadd1  8721  leadd2  8723  ltsubadd  8724  lesubadd  8726  ltaddsub2  8729  leaddsub2  8731  ltaddpos  8744  lesub2  8749  ltsub2  8751  ltnegcon1  8755  ltnegcon2  8756  lenegcon1  8758  lenegcon2  8759  addge01  8764  addge02  8765  suble0  8768  leaddle0  8769  lesub0  8771  eqord2  8776  sublt0d  8862  recexre  8870  reaplt  8880  reapltxor  8881  reapneg  8889  remulext1  8891  apreim  8895  apcotr  8899  apadd2  8901  addext  8902  apsub1  8934  mulcanap2d  8954  diveqap0  8976  diveqap1  8999  apmul2  9083  ltmul2  9150  lemul2  9151  ltmulgt11  9158  ltmulgt12  9159  gt0div  9164  ge0div  9165  ltmuldiv  9168  ltrec1  9182  lerec2  9183  ledivdiv  9184  ltdiv23  9186  lediv23  9187  suprleubex  9248  creur  9253  creui  9254  nn1suc  9276  nnrecl  9514  fcdmnn0fsuppg  9571  znnsub  9649  zgt0ge1  9656  zltlen  9677  nn0n0n1ge2b  9678  nn0le2is012  9681  btwnnz  9693  gtndiv  9694  prime  9698  eluz2  9880  indstr2  9962  negm  9968  nn01to3  9970  qapne  9992  qltlen  9993  qreccl  9995  irrmulap  10001  divlt1lt  10078  divle1le  10079  nnledivrp  10120  xnn0xadd0  10222  xltadd2  10232  xsubge0  10236  xlesubadd  10238  iccid  10280  elioc2  10291  elico2  10292  elicc2  10293  elfz2  10371  fzen  10400  fzsubel  10418  elfzp1  10431  fzpr  10436  fzrevral2  10465  fzrevral3  10466  nn0disj  10497  2ffzeq  10500  fzosplitsni  10606  fvinim0ffz  10612  ioo0  10646  ico0  10648  ioc0  10649  modq0  10718  negqmod0  10720  zmodidfzo  10742  frecuzrdgtcl  10801  nn0ennn  10822  nninfinf  10832  sq11  11001  nn0le2msqd  11109  nn0opth2d  11113  hashen  11175  zfz1isolem1  11240  zfz1iso  11241  csbwrdg  11282  wrdnval  11283  eqwrd  11293  ccat0  11312  ccatws1lenp1bg  11351  swrd0g  11380  swrdspsleq  11387  pfxeq  11416  pfxsuffeqwrdeq  11418  pfxsuff1eqwrdeq  11419  ccatopth2  11437  wrd2ind  11443  2shfti  11544  cjap  11620  cnreim  11692  rexfiuz  11703  rexanuz2  11705  abs00ap  11776  absext  11777  sqabs  11796  abslt  11802  absle  11803  absdiflt  11806  absdifle  11807  lenegsq  11809  minmax  11944  ltmininf  11949  mingeb  11956  xrminmax  11979  xrmin1inf  11981  xrmin2inf  11982  xrltmininf  11984  xrlemininf  11985  clim  11995  clim0c  12000  climrecvg1n  12062  zsumdc  12099  fsum2dlemstep  12149  binomlem  12198  pwm1geoserap1  12223  zproddc  12294  efieq  12450  sin01bnd  12472  cos01bnd  12473  dvdsval2  12505  modm1div  12515  zdvdsdc  12527  modmulconst  12538  dvdsaddr  12552  dvdsabseq  12562  fzocongeq  12573  zeo3  12583  odd2np1  12588  oddp1d2  12605  zob  12606  oddm1d2  12607  nnoddm1d2  12625  divalgb  12640  divalgmod  12642  modremain  12644  bits0  12663  bitsp1e  12667  bitsp1o  12668  bitscmp  12673  bitsinv1lem  12676  gcdn0gt0  12703  bezoutlemstep  12722  dvdssq  12756  nn0seqcvgd  12767  algcvgblem  12775  lcmdvds  12805  lcmgcdeq  12809  coprmdvds  12818  qredeq  12822  congr  12826  isprm2  12843  isprm3  12844  prmdvdsexp  12874  prmdvdsexpb  12875  prmexpb  12877  prmfac1  12878  cncongrprm  12883  oddpwdclemxy  12895  oddpwdclemodd  12898  qnumdenbi  12918  qnumgt0  12924  hashdvds  12947  crth  12950  fermltl  12960  modprminveq  12977  pcpremul  13020  pc2dvds  13057  pcz  13059  prmpwdvds  13082  4sqlem16  13133  ballotfilemfc0  13180  ballotfilemfcc  13181  ballotfilemodife  13188  ballotfilemrv1  13212  ballotfilemrv2  13213  ballotfilem1ri  13226  oddennn  13231  ctinfomlemom  13266  mgm1  13637  ismhm  13720  mhmpropd  13725  issubm  13731  issubm2  13732  grpsubrcan  13840  grplactcnv  13861  grp1  13865  eqgval  13980  eqgid  13983  quselbasg  13987  isghm  14000  conjnmzb  14037  iscmn  14050  eqgabl  14087  prdsbasmpt  14126  prdsbasmpt2  14134  rngmneg1  14190  rngmneg2  14191  rngpropd  14198  rngen1zr  14204  srgen1zr0  14235  ringideu  14264  ringpropd  14285  crngpropd  14286  dvdsrd  14343  dvdsr02  14354  opprunitd  14359  crngunit  14360  unitpropdg  14397  rhmunitinv  14427  isnzr2  14433  issubrng  14449  resrhm2b  14499  aprval  14533  aprunit  14534  isdrngtap  14548  opprdrng  14562  islmod  14569  islssm  14635  islssmg  14636  ellspsn  14695  isridl  14782  zrhrhmb  14900  zndvds  14927  znleval  14931  istopg  14994  eltg  15047  eltg2  15048  tgss2  15074  bastop1  15078  bastop2  15079  iscld  15098  isnei  15139  neiint  15140  iscn  15192  iscnp  15194  iscnp3  15198  tgcn  15203  ssidcn  15205  lmbr2  15209  lmbrf  15210  cnnei  15227  cnrest2  15231  eltx  15254  imasnopn  15294  ispsmet  15318  ismet  15339  isxmet  15340  metn0  15373  xmetres2  15374  elbl3ps  15389  elbl3  15390  xblpnfps  15393  xblpnf  15394  elmopn2  15444  metss  15489  bdxmet  15496  metrest  15501  xmetxp  15502  xmetxpbl  15503  metcnp3  15506  metcnp  15507  metcnp2  15508  metcn  15509  txmetcnp  15513  txmetcn  15514  metcnpd  15515  bl2ioo  15545  addcncntoplem  15556  elcncf  15568  elcncf2  15569  ivthdec  15639  ellimc3apf  15655  cnlimcim  15666  dveflem  15721  ply1termlem  15737  sincosq2sgn  15822  sinq12gt0  15825  logltb  15869  ltexp2  15936  wilthlem1  15978  lgsdilem  16030  lgsdir2lem4  16034  lgsdir2  16036  lgsne0  16041  lgsabs1  16042  gausslemma2dlem3  16066  gausslemma2dlem7  16071  lgseisenlem3  16075  lgsquad3  16087  2lgslem1a  16091  2lgslem3c  16098  2lgslem3d  16099  2lgsoddprmlem4  16115  2sqlem7  16124  2sqlem8a  16125  uhgreq12g  16201  isuhgropm  16206  uhgr0e  16207  upgrop  16229  uhgrvtxedgiedgb  16268  isuspgropen  16289  isusgropen  16290  uhgr2edg  16331  issubgr2  16383  uhgrspansubgrlem  16401  vtxd0nedgbfi  16424  1loopgrvd0fi  16431  iswlk  16448  upgriswlkdc  16485  istrl  16510  iseupth  16572  eupth2lem2dc  16584  eupth2lem3lem3fi  16595  eupth2lem3lem4fi  16598  eupth2lem3lem7fi  16599  cbvrald  16700  bj-nalset  16805  bj-sels  16824  bj-nnelirr  16863  isomninnlem  16954  iswomninnlem  16974  iswomni0  16976  ismkvnnlem  16977