Theorem bitrd 187

Description: Deduction form of bitri 183. (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 179	. . 3 |- ( ( ph -> ps ) <-> ( ph -> ch ) )
3		bitrd.2	. . . 4 |- ( ph -> ( ch <-> th ) )
4	3	pm5.74i 179	. . 3 |- ( ( ph -> ch ) <-> ( ph -> th ) )
5	2, 4	bitri 183	. 2 |- ( ( ph -> ps ) <-> ( ph -> th ) )
6	5	pm5.74ri 180	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:  bitr2d  188  bitr3d  189  bitr4d  190  syl5bb  191  bitrdi  195  3bitrd  213  3bitr2d  215  3bitr3d  217  3bitr4d  219  imbi12d  233  bibi12d  234  sylan9bb  458  anbi12d  465  orbi12d  783  con1biidc  867  pm4.54dc  892  dn1dc  950  dedlem0a  958  xorbi12d  1372  nbbndc  1384  eleq12d  2236  neeq12d  2355  neleq12d  2436  raleqbi1dv  2668  rexeqbi1dv  2669  reueqd  2670  rmoeqd  2671  raleqbidv  2672  rexeqbidv  2673  raleqbidva  2674  rexeqbidva  2675  eueq3dc  2899  sbc19.21g  3018  sbcabel  3031  sbcel1g  3063  sbceq1g  3064  sbcel2g  3065  sbceq2g  3066  sbccsb2g  3074  sbcco3g  3101  sseq12d  3172  raaanlem  3513  sbcssg  3517  ralsng  3615  2ralunsn  3777  csbunig  3796  disjeq12d  3967  breq123d  3995  sbcbr12g  4036  sbcbr1g  4037  sbcbr2g  4038  treq  4085  nalset  4111  exmidsssn  4180  copsex4g  4224  sucelon  4479  posng  4675  csbxpg  4684  sbcrel  4689  csbcnvg  4787  eliniseg  4973  brcodir  4990  csbrng  5064  sbcfung  5211  fneq12d  5279  feq12d  5326  feq123d  5327  sbcfng  5334  sbcfg  5335  f1osng  5472  csbfv12g  5521  funimass4  5536  dmfco  5553  eqfnfv  5582  eqfnfv2  5583  fneqeql2  5593  fvimacnvi  5598  funimass3  5600  fniniseg  5604  rexsupp  5608  unpreima  5609  ralrnmpt  5626  rexrnmpt  5627  dffo3  5631  fmptco  5650  fressnfv  5671  eufnfv  5714  foima2  5719  fnunirn  5734  dff13  5735  f1elima  5740  cocan1  5754  cocan2  5755  fliftel  5760  fliftf  5766  isoresbr  5776  isoini  5785  f1oiso  5793  f1ofveu  5829  mpoeq123dva  5899  ovid  5954  ov  5957  ovg  5976  ovelrn  5986  caovord2d  6007  ofrfval2  6065  offveqb  6068  eqop  6142  reldm  6151  f1od2  6199  mpoxopoveq  6204  mpoxopovel  6205  tpostpos  6228  smoiso  6266  frecabcl  6363  frecsuclem  6370  nnaordr  6474  nnaword  6475  nnaordex  6491  ereq1  6504  brdifun  6524  erth2  6542  qliftfun  6579  brecop  6587  elmapg  6623  elpmg  6626  dom2lem  6734  xpcomco  6788  php5fin  6844  elfi2  6933  supisolem  6969  inflbti  6985  inl11  7026  ismkvnex  7115  mkvprop  7118  exmidfodomrlemreseldju  7152  ltapig  7275  ltmpig  7276  nlt1pig  7278  mulcmpblnq  7305  ltsonq  7335  lt2addnq  7341  lt2mulnq  7342  archnqq  7354  prarloclemarch  7355  ltrnqg  7357  mulcmpblnq0  7381  preqlu  7409  genpdflem  7444  addnqprllem  7464  addnqprulem  7465  addlocprlemgt  7471  appdivnq  7500  mulnqprl  7505  mulnqpru  7506  mullocprlem  7507  distrlem4prl  7521  distrlem4pru  7522  1idprl  7527  1idpru  7528  ltexprlemloc  7544  cauappcvgprlemladdrl  7594  cauappcvgprlemladd  7595  cauappcvgprlem1  7596  archrecnq  7600  caucvgprlemnkj  7603  caucvgprprlemexb  7644  addcmpblnr  7676  lttrsr  7699  ltsosr  7701  ltasrg  7707  mulextsr1  7718  srpospr  7720  caucvgsrlemcau  7730  caucvgsrlemgt1  7732  caucvgsrlemoffres  7737  map2psrprg  7742  ltresr  7776  axcaucvglemres  7836  eqlelt  7981  cnegexlem1  8069  negeu  8085  subadd2  8098  subcan2  8119  addrsub  8265  ltaddneg  8318  ltaddnegr  8319  ltadd1  8323  leadd2  8325  ltsubadd  8326  lesubadd  8328  ltaddsub2  8331  leaddsub2  8333  ltaddpos  8346  lesub2  8351  ltsub2  8353  ltnegcon1  8357  ltnegcon2  8358  lenegcon1  8360  lenegcon2  8361  addge01  8366  addge02  8367  suble0  8370  leaddle0  8371  lesub0  8373  eqord2  8378  sublt0d  8464  recexre  8472  reaplt  8482  reapltxor  8483  reapneg  8491  remulext1  8493  apreim  8497  apcotr  8501  apadd2  8503  addext  8504  apsub1  8536  mulcanap2d  8555  diveqap0  8574  diveqap1  8597  apmul2  8681  ltmul2  8747  lemul2  8748  ltmulgt11  8755  ltmulgt12  8756  gt0div  8761  ge0div  8762  ltmuldiv  8765  ltrec1  8779  lerec2  8780  ledivdiv  8781  ltdiv23  8783  lediv23  8784  suprleubex  8845  creur  8850  creui  8851  nn1suc  8872  nnrecl  9108  znnsub  9238  zgt0ge1  9245  zltlen  9265  nn0n0n1ge2b  9266  nn0le2is012  9269  btwnnz  9281  gtndiv  9282  prime  9286  eluz2  9468  indstr2  9543  negm  9549  nn01to3  9551  qapne  9573  qltlen  9574  qreccl  9576  divlt1lt  9656  divle1le  9657  nnledivrp  9698  xnn0xadd0  9799  xltadd2  9809  xsubge0  9813  xlesubadd  9815  iccid  9857  elioc2  9868  elico2  9869  elicc2  9870  elfz2  9947  fzen  9974  fzsubel  9991  elfzp1  10003  fzpr  10008  fzrevral2  10037  fzrevral3  10038  nn0disj  10069  2ffzeq  10072  fzosplitsni  10166  fvinim0ffz  10172  ioo0  10191  ico0  10193  ioc0  10194  modq0  10260  negqmod0  10262  zmodidfzo  10284  frecuzrdgtcl  10343  nn0ennn  10364  sq11  10523  nn0le2msqd  10628  nn0opth2d  10632  hashen  10693  zfz1isolem1  10749  zfz1iso  10750  2shfti  10769  cjap  10844  cnreim  10916  rexfiuz  10927  rexanuz2  10929  abs00ap  11000  absext  11001  sqabs  11020  abslt  11026  absle  11027  absdiflt  11030  absdifle  11031  lenegsq  11033  minmax  11167  ltmininf  11172  mingeb  11179  xrminmax  11202  xrmin1inf  11204  xrmin2inf  11205  xrltmininf  11207  xrlemininf  11208  clim  11218  clim0c  11223  climrecvg1n  11285  zsumdc  11321  fsum2dlemstep  11371  binomlem  11420  pwm1geoserap1  11445  zproddc  11516  efieq  11672  sin01bnd  11694  cos01bnd  11695  dvdsval2  11726  modm1div  11736  zdvdsdc  11748  modmulconst  11759  dvdsaddr  11773  dvdsabseq  11781  fzocongeq  11792  zeo3  11801  odd2np1  11806  oddp1d2  11823  zob  11824  oddm1d2  11825  nnoddm1d2  11843  divalgb  11858  divalgmod  11860  modremain  11862  gcdn0gt0  11907  bezoutlemstep  11926  dvdssq  11960  nn0seqcvgd  11969  algcvgblem  11977  lcmdvds  12007  lcmgcdeq  12011  coprmdvds  12020  qredeq  12024  congr  12028  isprm2  12045  isprm3  12046  prmdvdsexp  12076  prmdvdsexpb  12077  prmexpb  12079  prmfac1  12080  cncongrprm  12085  oddpwdclemxy  12097  oddpwdclemodd  12100  qnumdenbi  12120  qnumgt0  12126  hashdvds  12149  crth  12152  fermltl  12162  modprminveq  12178  pcpremul  12221  pc2dvds  12257  pcz  12259  prmpwdvds  12281  oddennn  12321  ctinfomlemom  12356  istopg  12597  eltg  12652  eltg2  12653  tgss2  12679  bastop1  12683  bastop2  12684  iscld  12703  isnei  12744  neiint  12745  iscn  12797  iscnp  12799  iscnp3  12803  tgcn  12808  ssidcn  12810  lmbr2  12814  lmbrf  12815  cnnei  12832  cnrest2  12836  eltx  12859  imasnopn  12899  ispsmet  12923  ismet  12944  isxmet  12945  metn0  12978  xmetres2  12979  elbl3ps  12994  elbl3  12995  xblpnfps  12998  xblpnf  12999  elmopn2  13049  metss  13094  bdxmet  13101  metrest  13106  xmetxp  13107  xmetxpbl  13108  metcnp3  13111  metcnp  13112  metcnp2  13113  metcn  13114  txmetcnp  13118  txmetcn  13119  metcnpd  13120  bl2ioo  13142  addcncntoplem  13151  elcncf  13160  elcncf2  13161  ivthdec  13222  ellimc3apf  13229  cnlimcim  13240  dveflem  13287  sincosq2sgn  13348  sinq12gt0  13351  logltb  13395  ltexp2  13460  lgsdilem  13528  lgsdir2lem4  13532  lgsdir2  13534  lgsne0  13539  lgsabs1  13540  2sqlem7  13557  2sqlem8a  13558  cbvrald  13629  bj-nalset  13737  bj-sels  13756  bj-nnelirr  13795  isomninnlem  13869  iswomninnlem  13888  iswomni0  13890  ismkvnnlem  13891