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 ) )

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:  bitr2d  189  bitr3d  190  bitr4d  191  bitrid  192  bitrdi  196  3bitrd  214  3bitr2d  216  3bitr3d  218  3bitr4d  220  imbi12d  234  bibi12d  235  sylan9bb  466  anbi12d  477  orbi12d  805  con1biidc  889  pm4.54dc  914  dn1dc  973  dedlem0a  981  dfifp3dc  995  dfifp4dc  996  dfifp5dc  997  3bior2fd  1395  xorbi12d  1431  nbbndc  1443  eleq12d  2309  neeq12d  2440  neleq12d  2521  raleqbi1dv  2761  rexeqbi1dv  2762  reueqd  2763  rmoeqd  2764  raleqbidv  2765  rexeqbidv  2766  raleqbidva  2767  rexeqbidva  2768  eueq3dc  3000  sbc19.21g  3120  sbcabel  3134  sbcel1g  3166  sbceq1g  3167  sbcel2g  3168  sbceq2g  3169  sbccsb2g  3177  sbcco3g  3205  sseq12d  3279  raaanlem  3632  sbcssg  3636  ralsng  3749  2ralunsn  3924  csbunig  3943  disjeq12d  4115  breq123d  4144  sbcbr12g  4186  sbcbr1g  4187  sbcbr2g  4188  treq  4235  nalset  4263  exmidsssn  4339  copsex4g  4387  onsucb  4650  posng  4847  csbxpg  4856  sbcrel  4861  csbcnvg  4964  eliniseg  5157  brcodir  5175  csbrng  5249  sbcfung  5401  fneq12d  5473  feq12d  5523  feq123d  5524  sbcfng  5531  sbcfg  5532  f1osng  5682  csbfv12g  5736  funimass4  5753  dmfco  5773  eqfnfv  5806  eqfnfv2  5807  fneqeql2  5818  fvimacnvi  5823  funimass3  5825  fniniseg  5829  unpreima  5833  ralrnmpt  5850  rexrnmpt  5851  dffo3  5855  fmptco  5874  fressnfv  5902  eufnfv  5949  foima2  5957  fnunirn  5973  dff13  5974  f1elima  5979  cocan1  5993  cocan2  5994  fliftel  5999  fliftf  6005  isoresbr  6015  isoini  6024  f1oiso  6032  f1ofveu  6073  mpoeq123dva  6149  ovid  6205  ov  6208  ovg  6228  ovelrn  6238  caovord2d  6259  ofrfval2  6319  offveqb  6322  eqop  6411  reldm  6420  f1od2  6471  suppval1  6479  suppssrst  6501  suppssrgst  6502  mpoxopoveq  6511  mpoxopovel  6512  tpostpos  6535  smoiso  6573  frecabcl  6670  frecsuclem  6677  nnaordr  6783  nnaword  6784  nnaordex  6801  ereq1  6814  brdifun  6834  erth2  6854  qliftfun  6891  brecop  6899  elmapg  6935  elpmg  6938  mapsnd  6970  dom2lem  7058  xpcomco  7124  pw2f1odclem  7134  php5fin  7186  funisfsupp  7291  ffsuppbi  7300  elfi2  7306  supisolem  7348  inflbti  7364  inl11  7405  ismkvnex  7495  mkvprop  7498  nninfwlporlemd  7512  exmidfodomrlemreseldju  7552  ltapig  7705  ltmpig  7706  nlt1pig  7708  mulcmpblnq  7735  ltsonq  7765  lt2addnq  7771  lt2mulnq  7772  archnqq  7784  prarloclemarch  7785  ltrnqg  7787  mulcmpblnq0  7811  preqlu  7839  genpdflem  7874  addnqprllem  7894  addnqprulem  7895  addlocprlemgt  7901  appdivnq  7930  mulnqprl  7935  mulnqpru  7936  mullocprlem  7937  distrlem4prl  7951  distrlem4pru  7952  1idprl  7957  1idpru  7958  ltexprlemloc  7974  cauappcvgprlemladdrl  8024  cauappcvgprlemladd  8025  cauappcvgprlem1  8026  archrecnq  8030  caucvgprlemnkj  8033  caucvgprprlemexb  8074  addcmpblnr  8106  lttrsr  8129  ltsosr  8131  ltasrg  8137  mulextsr1  8148  srpospr  8150  caucvgsrlemcau  8160  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  map2psrprg  8172  ltresr  8206  axcaucvglemres  8266  eqlelt  8412  cnegexlem1  8501  negeu  8517  subadd2  8530  subcan2  8551  addrsub  8697  ltaddneg  8752  ltaddnegr  8753  ltadd1  8757  leadd2  8759  ltsubadd  8760  lesubadd  8762  ltaddsub2  8765  leaddsub2  8767  ltaddpos  8780  lesub2  8785  ltsub2  8787  ltnegcon1  8791  ltnegcon2  8792  lenegcon1  8794  lenegcon2  8795  addge01  8800  addge02  8801  suble0  8804  leaddle0  8805  lesub0  8807  eqord2  8812  sublt0d  8898  recexre  8906  reaplt  8916  reapltxor  8917  reapneg  8925  remulext1  8927  apreim  8931  apcotr  8935  apadd2  8937  addext  8938  apsub1  8970  mulcanap2d  8990  diveqap0  9012  diveqap1  9035  apmul2  9119  ltmul2  9186  lemul2  9187  ltmulgt11  9194  ltmulgt12  9195  gt0div  9200  ge0div  9201  ltmuldiv  9204  ltrec1  9218  lerec2  9219  ledivdiv  9220  ltdiv23  9222  lediv23  9223  suprleubex  9284  creur  9289  creui  9290  nn1suc  9323  nnrecl  9561  fcdmnn0fsuppg  9618  znnsub  9696  zgt0ge1  9703  zltlen  9724  nn0n0n1ge2b  9725  nn0le2is012  9728  btwnnz  9740  gtndiv  9741  prime  9745  eluz2  9927  indstr2  10009  negm  10015  nn01to3  10017  qapne  10039  qltlen  10040  qreccl  10042  irrmulap  10048  divlt1lt  10125  divle1le  10126  nnledivrp  10167  xnn0xadd0  10269  xltadd2  10279  xsubge0  10283  xlesubadd  10285  iccid  10327  elioc2  10338  elico2  10339  elicc2  10340  elfz2  10418  fzen  10447  fzsubel  10466  elfzp1  10479  fzpr  10484  fzrevral2  10513  fzrevral3  10514  nn0disj  10545  2ffzeq  10548  fzosplitsni  10654  fvinim0ffz  10660  ioo0  10694  ico0  10696  ioc0  10697  modq0  10766  negqmod0  10768  zmodidfzo  10790  frecuzrdgtcl  10849  nn0ennn  10870  nninfinf  10880  sq11  11049  nn0le2msqd  11157  nn0opth2d  11161  hashen  11223  zfz1isolem1  11292  zfz1iso  11293  csbwrdg  11334  wrdnval  11335  eqwrd  11345  ccat0  11364  ccatws1lenp1bg  11403  swrd0g  11432  swrdspsleq  11439  pfxeq  11468  pfxsuffeqwrdeq  11470  pfxsuff1eqwrdeq  11471  ccatopth2  11489  wrd2ind  11495  2shfti  11596  cjap  11672  cnreim  11744  rexfiuz  11755  rexanuz2  11757  abs00ap  11828  absext  11829  sqabs  11848  abslt  11854  absle  11855  absdiflt  11858  absdifle  11859  lenegsq  11861  minmax  11996  ltmininf  12001  mingeb  12008  xrminmax  12031  xrmin1inf  12033  xrmin2inf  12034  xrltmininf  12036  xrlemininf  12037  clim  12047  clim0c  12052  climrecvg1n  12114  zsumdc  12151  fsum2dlemstep  12201  binomlem  12250  pwm1geoserap1  12275  zproddc  12346  efieq  12502  sin01bnd  12524  cos01bnd  12525  dvdsval2  12557  modm1div  12567  zdvdsdc  12579  modmulconst  12590  dvdsaddr  12604  dvdsabseq  12614  fzocongeq  12625  zeo3  12635  odd2np1  12640  oddp1d2  12657  zob  12658  oddm1d2  12659  nnoddm1d2  12677  divalgb  12692  divalgmod  12694  modremain  12696  bits0  12715  bitsp1e  12719  bitsp1o  12720  bitscmp  12725  bitsinv1lem  12728  gcdn0gt0  12755  bezoutlemstep  12774  dvdssq  12808  nn0seqcvgd  12819  algcvgblem  12827  lcmdvds  12857  lcmgcdeq  12861  coprmdvds  12870  qredeq  12874  congr  12878  isprm2  12895  isprm3  12896  prmdvdsexp  12926  prmdvdsexpb  12927  prmexpb  12929  prmfac1  12930  cncongrprm  12935  oddpwdclemxy  12947  oddpwdclemodd  12950  qnumdenbi  12970  qnumgt0  12976  hashdvds  12999  crth  13002  fermltl  13012  modprminveq  13029  pcpremul  13072  pc2dvds  13109  pcz  13111  prmpwdvds  13134  4sqlem16  13185  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemodife  13240  ballotfilemrv1  13264  ballotfilemrv2  13265  ballotfilem1ri  13278  oddennn  13283  ctinfomlemom  13318  mgm1  13690  ismhm  13768  mhmpropd  13773  issubm  13779  issubm2  13780  grpsubrcan  13886  grplactcnv  13907  grp1  13911  eqgval  14026  eqgid  14029  quselbasg  14033  isghm  14046  conjnmzb  14083  iscmn  14096  eqgabl  14134  prdsbasmpt  14180  prdsbasmpt2  14188  rngmneg1  14246  rngmneg2  14247  rngpropd  14254  rngen1zr  14260  srgen1zr0  14292  ringideu  14321  ringpropd  14343  crngpropd  14344  dvdsrd  14401  dvdsr02  14412  opprunitd  14417  crngunit  14418  unitpropdg  14455  rhmunitinv  14485  isnzr2  14491  issubrng  14507  resrhm2b  14557  aprval  14591  aprunit  14592  isdrngtap  14606  opprdrng  14620  islmod  14627  islssm  14694  islssmg  14695  ellspsn  14754  isridl  14841  zrhrhmb  14957  zndvds  14984  znleval  14988  isassa  15002  istopg  15100  eltg  15153  eltg2  15154  tgss2  15180  bastop1  15184  bastop2  15185  iscld  15204  isnei  15245  neiint  15246  iscn  15298  iscnp  15300  iscnp3  15304  tgcn  15309  ssidcn  15311  lmbr2  15315  lmbrf  15316  cnnei  15333  cnrest2  15337  eltx  15360  imasnopn  15400  ispsmet  15424  ismet  15445  isxmet  15446  metn0  15479  xmetres2  15480  elbl3ps  15495  elbl3  15496  xblpnfps  15499  xblpnf  15500  elmopn2  15550  metss  15595  bdxmet  15602  metrest  15607  xmetxp  15608  xmetxpbl  15609  metcnp3  15612  metcnp  15613  metcnp2  15614  metcn  15615  txmetcnp  15619  txmetcn  15620  metcnpd  15621  bl2ioo  15651  addcncntoplem  15662  elcncf  15674  elcncf2  15675  ivthdec  15745  ellimc3apf  15761  cnlimcim  15772  dveflem  15827  ply1termlem  15843  sincosq2sgn  15928  sinq12gt0  15931  logltb  15975  ltexp2  16043  birthdaylem3  16089  wilthlem1  16094  lgsdilem  16146  lgsdir2lem4  16150  lgsdir2  16152  lgsne0  16157  lgsabs1  16158  gausslemma2dlem3  16182  gausslemma2dlem7  16187  lgseisenlem3  16191  lgsquad3  16203  2lgslem1a  16207  2lgslem3c  16214  2lgslem3d  16215  2lgsoddprmlem4  16231  2sqlem7  16240  2sqlem8a  16241  uhgreq12g  16317  isuhgropm  16322  uhgr0e  16323  upgrop  16345  uhgrvtxedgiedgb  16384  isuspgropen  16405  isusgropen  16406  uhgr2edg  16447  issubgr2  16499  uhgrspansubgrlem  16517  vtxd0nedgbfi  16540  1loopgrvd0fi  16547  iswlk  16564  upgriswlkdc  16601  istrl  16626  iseupth  16688  eupth2lem2dc  16700  eupth2lem3lem3fi  16711  eupth2lem3lem4fi  16714  eupth2lem3lem7fi  16715  cbvrald  16816  bj-nalset  16921  bj-sels  16940  bj-nnelirr  16979  stnot  17039  isomninnlem  17079  iswomninnlem  17099  iswomni0  17101  ismkvnnlem  17102