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  8464  negeu  8480  subadd2  8493  subcan2  8514  addrsub  8660  ltaddneg  8715  ltaddnegr  8716  ltadd1  8720  leadd2  8722  ltsubadd  8723  lesubadd  8725  ltaddsub2  8728  leaddsub2  8730  ltaddpos  8743  lesub2  8748  ltsub2  8750  ltnegcon1  8754  ltnegcon2  8755  lenegcon1  8757  lenegcon2  8758  addge01  8763  addge02  8764  suble0  8767  leaddle0  8768  lesub0  8770  eqord2  8775  sublt0d  8861  recexre  8869  reaplt  8879  reapltxor  8880  reapneg  8888  remulext1  8890  apreim  8894  apcotr  8898  apadd2  8900  addext  8901  apsub1  8933  mulcanap2d  8953  diveqap0  8973  diveqap1  8996  apmul2  9080  ltmul2  9147  lemul2  9148  ltmulgt11  9155  ltmulgt12  9156  gt0div  9161  ge0div  9162  ltmuldiv  9165  ltrec1  9179  lerec2  9180  ledivdiv  9181  ltdiv23  9183  lediv23  9184  suprleubex  9245  creur  9250  creui  9251  nn1suc  9273  nnrecl  9511  fcdmnn0fsuppg  9568  znnsub  9646  zgt0ge1  9653  zltlen  9674  nn0n0n1ge2b  9675  nn0le2is012  9678  btwnnz  9690  gtndiv  9691  prime  9695  eluz2  9877  indstr2  9959  negm  9965  nn01to3  9967  qapne  9989  qltlen  9990  qreccl  9992  irrmulap  9998  divlt1lt  10075  divle1le  10076  nnledivrp  10117  xnn0xadd0  10219  xltadd2  10229  xsubge0  10233  xlesubadd  10235  iccid  10277  elioc2  10288  elico2  10289  elicc2  10290  elfz2  10368  fzen  10397  fzsubel  10415  elfzp1  10428  fzpr  10433  fzrevral2  10462  fzrevral3  10463  nn0disj  10494  2ffzeq  10497  fzosplitsni  10603  fvinim0ffz  10609  ioo0  10643  ico0  10645  ioc0  10646  modq0  10715  negqmod0  10717  zmodidfzo  10739  frecuzrdgtcl  10798  nn0ennn  10819  nninfinf  10829  sq11  10998  nn0le2msqd  11106  nn0opth2d  11110  hashen  11172  zfz1isolem1  11237  zfz1iso  11238  csbwrdg  11279  wrdnval  11280  eqwrd  11290  ccat0  11309  ccatws1lenp1bg  11348  swrd0g  11377  swrdspsleq  11384  pfxeq  11413  pfxsuffeqwrdeq  11415  pfxsuff1eqwrdeq  11416  ccatopth2  11434  wrd2ind  11440  2shfti  11541  cjap  11616  cnreim  11688  rexfiuz  11699  rexanuz2  11701  abs00ap  11772  absext  11773  sqabs  11792  abslt  11798  absle  11799  absdiflt  11802  absdifle  11803  lenegsq  11805  minmax  11940  ltmininf  11945  mingeb  11952  xrminmax  11975  xrmin1inf  11977  xrmin2inf  11978  xrltmininf  11980  xrlemininf  11981  clim  11991  clim0c  11996  climrecvg1n  12058  zsumdc  12095  fsum2dlemstep  12145  binomlem  12194  pwm1geoserap1  12219  zproddc  12290  efieq  12446  sin01bnd  12468  cos01bnd  12469  dvdsval2  12501  modm1div  12511  zdvdsdc  12523  modmulconst  12534  dvdsaddr  12548  dvdsabseq  12558  fzocongeq  12569  zeo3  12579  odd2np1  12584  oddp1d2  12601  zob  12602  oddm1d2  12603  nnoddm1d2  12621  divalgb  12636  divalgmod  12638  modremain  12640  bits0  12659  bitsp1e  12663  bitsp1o  12664  bitscmp  12669  bitsinv1lem  12672  gcdn0gt0  12699  bezoutlemstep  12718  dvdssq  12752  nn0seqcvgd  12763  algcvgblem  12771  lcmdvds  12801  lcmgcdeq  12805  coprmdvds  12814  qredeq  12818  congr  12822  isprm2  12839  isprm3  12840  prmdvdsexp  12870  prmdvdsexpb  12871  prmexpb  12873  prmfac1  12874  cncongrprm  12879  oddpwdclemxy  12891  oddpwdclemodd  12894  qnumdenbi  12914  qnumgt0  12920  hashdvds  12943  crth  12946  fermltl  12956  modprminveq  12973  pcpremul  13016  pc2dvds  13053  pcz  13055  prmpwdvds  13078  4sqlem16  13129  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemodife  13184  ballotfilemrv1  13208  ballotfilemrv2  13209  ballotfilem1ri  13222  oddennn  13227  ctinfomlemom  13262  mgm1  13633  ismhm  13716  mhmpropd  13721  issubm  13727  issubm2  13728  grpsubrcan  13836  grplactcnv  13857  grp1  13861  eqgval  13976  eqgid  13979  quselbasg  13983  isghm  13996  conjnmzb  14033  iscmn  14046  eqgabl  14083  prdsbasmpt  14122  prdsbasmpt2  14130  rngmneg1  14186  rngmneg2  14187  rngpropd  14194  rngen1zr  14200  srgen1zr0  14231  ringideu  14260  ringpropd  14281  crngpropd  14282  dvdsrd  14339  dvdsr02  14350  opprunitd  14355  crngunit  14356  unitpropdg  14393  rhmunitinv  14423  isnzr2  14429  issubrng  14445  resrhm2b  14495  aprval  14529  aprunit  14530  isdrngtap  14544  opprdrng  14558  islmod  14565  islssm  14631  islssmg  14632  ellspsn  14691  isridl  14778  zrhrhmb  14896  zndvds  14923  znleval  14927  istopg  14990  eltg  15043  eltg2  15044  tgss2  15070  bastop1  15074  bastop2  15075  iscld  15094  isnei  15135  neiint  15136  iscn  15188  iscnp  15190  iscnp3  15194  tgcn  15199  ssidcn  15201  lmbr2  15205  lmbrf  15206  cnnei  15223  cnrest2  15227  eltx  15250  imasnopn  15290  ispsmet  15314  ismet  15335  isxmet  15336  metn0  15369  xmetres2  15370  elbl3ps  15385  elbl3  15386  xblpnfps  15389  xblpnf  15390  elmopn2  15440  metss  15485  bdxmet  15492  metrest  15497  xmetxp  15498  xmetxpbl  15499  metcnp3  15502  metcnp  15503  metcnp2  15504  metcn  15505  txmetcnp  15509  txmetcn  15510  metcnpd  15511  bl2ioo  15541  addcncntoplem  15552  elcncf  15564  elcncf2  15565  ivthdec  15635  ellimc3apf  15651  cnlimcim  15662  dveflem  15717  ply1termlem  15733  sincosq2sgn  15818  sinq12gt0  15821  logltb  15865  ltexp2  15932  wilthlem1  15974  lgsdilem  16026  lgsdir2lem4  16030  lgsdir2  16032  lgsne0  16037  lgsabs1  16038  gausslemma2dlem3  16062  gausslemma2dlem7  16067  lgseisenlem3  16071  lgsquad3  16083  2lgslem1a  16087  2lgslem3c  16094  2lgslem3d  16095  2lgsoddprmlem4  16111  2sqlem7  16120  2sqlem8a  16121  uhgreq12g  16197  isuhgropm  16202  uhgr0e  16203  upgrop  16225  uhgrvtxedgiedgb  16264  isuspgropen  16285  isusgropen  16286  uhgr2edg  16327  issubgr2  16379  uhgrspansubgrlem  16397  vtxd0nedgbfi  16420  1loopgrvd0fi  16427  iswlk  16444  upgriswlkdc  16481  istrl  16506  iseupth  16568  eupth2lem2dc  16580  eupth2lem3lem3fi  16591  eupth2lem3lem4fi  16594  eupth2lem3lem7fi  16595  cbvrald  16686  bj-nalset  16791  bj-sels  16810  bj-nnelirr  16849  isomninnlem  16940  iswomninnlem  16960  iswomni0  16962  ismkvnnlem  16963