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	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitrd.2	⊢ (𝜑 → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
bitrd	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitrd

Step	Hyp	Ref	Expression
1		bitrd.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	pm5.74i 180	. . 3 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
3		bitrd.2	. . . 4 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	3	pm5.74i 180	. . 3 ⊢ ((𝜑 → 𝜒) ↔ (𝜑 → 𝜃))
5	2, 4	bitri 184	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜃))
6	5	pm5.74ri 181	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

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  794  con1biidc  878  pm4.54dc  903  dn1dc  962  dedlem0a  970  xorbi12d  1393  nbbndc  1405  eleq12d  2267  neeq12d  2387  neleq12d  2468  raleqbi1dv  2705  rexeqbi1dv  2706  reueqd  2707  rmoeqd  2708  raleqbidv  2709  rexeqbidv  2710  raleqbidva  2711  rexeqbidva  2712  eueq3dc  2938  sbc19.21g  3058  sbcabel  3071  sbcel1g  3103  sbceq1g  3104  sbcel2g  3105  sbceq2g  3106  sbccsb2g  3114  sbcco3g  3142  sseq12d  3215  raaanlem  3556  sbcssg  3560  ralsng  3663  2ralunsn  3829  csbunig  3848  disjeq12d  4020  breq123d  4048  sbcbr12g  4089  sbcbr1g  4090  sbcbr2g  4091  treq  4138  nalset  4164  exmidsssn  4236  copsex4g  4281  onsucb  4540  posng  4736  csbxpg  4745  sbcrel  4750  csbcnvg  4851  eliniseg  5040  brcodir  5058  csbrng  5132  sbcfung  5283  fneq12d  5351  feq12d  5400  feq123d  5401  sbcfng  5408  sbcfg  5409  f1osng  5548  csbfv12g  5599  funimass4  5614  dmfco  5632  eqfnfv  5662  eqfnfv2  5663  fneqeql2  5674  fvimacnvi  5679  funimass3  5681  fniniseg  5685  rexsupp  5689  unpreima  5690  ralrnmpt  5707  rexrnmpt  5708  dffo3  5712  fmptco  5731  fressnfv  5752  eufnfv  5796  foima2  5801  fnunirn  5817  dff13  5818  f1elima  5823  cocan1  5837  cocan2  5838  fliftel  5843  fliftf  5849  isoresbr  5859  isoini  5868  f1oiso  5876  f1ofveu  5913  mpoeq123dva  5987  ovid  6043  ov  6046  ovg  6066  ovelrn  6076  caovord2d  6097  ofrfval2  6156  offveqb  6159  eqop  6244  reldm  6253  f1od2  6302  mpoxopoveq  6307  mpoxopovel  6308  tpostpos  6331  smoiso  6369  frecabcl  6466  frecsuclem  6473  nnaordr  6577  nnaword  6578  nnaordex  6595  ereq1  6608  brdifun  6628  erth2  6648  qliftfun  6685  brecop  6693  elmapg  6729  elpmg  6732  dom2lem  6840  xpcomco  6894  pw2f1odclem  6904  php5fin  6952  elfi2  7047  supisolem  7083  inflbti  7099  inl11  7140  ismkvnex  7230  mkvprop  7233  nninfwlporlemd  7247  exmidfodomrlemreseldju  7281  ltapig  7424  ltmpig  7425  nlt1pig  7427  mulcmpblnq  7454  ltsonq  7484  lt2addnq  7490  lt2mulnq  7491  archnqq  7503  prarloclemarch  7504  ltrnqg  7506  mulcmpblnq0  7530  preqlu  7558  genpdflem  7593  addnqprllem  7613  addnqprulem  7614  addlocprlemgt  7620  appdivnq  7649  mulnqprl  7654  mulnqpru  7655  mullocprlem  7656  distrlem4prl  7670  distrlem4pru  7671  1idprl  7676  1idpru  7677  ltexprlemloc  7693  cauappcvgprlemladdrl  7743  cauappcvgprlemladd  7744  cauappcvgprlem1  7745  archrecnq  7749  caucvgprlemnkj  7752  caucvgprprlemexb  7793  addcmpblnr  7825  lttrsr  7848  ltsosr  7850  ltasrg  7856  mulextsr1  7867  srpospr  7869  caucvgsrlemcau  7879  caucvgsrlemgt1  7881  caucvgsrlemoffres  7886  map2psrprg  7891  ltresr  7925  axcaucvglemres  7985  eqlelt  8132  cnegexlem1  8220  negeu  8236  subadd2  8249  subcan2  8270  addrsub  8416  ltaddneg  8470  ltaddnegr  8471  ltadd1  8475  leadd2  8477  ltsubadd  8478  lesubadd  8480  ltaddsub2  8483  leaddsub2  8485  ltaddpos  8498  lesub2  8503  ltsub2  8505  ltnegcon1  8509  ltnegcon2  8510  lenegcon1  8512  lenegcon2  8513  addge01  8518  addge02  8519  suble0  8522  leaddle0  8523  lesub0  8525  eqord2  8530  sublt0d  8616  recexre  8624  reaplt  8634  reapltxor  8635  reapneg  8643  remulext1  8645  apreim  8649  apcotr  8653  apadd2  8655  addext  8656  apsub1  8688  mulcanap2d  8708  diveqap0  8728  diveqap1  8751  apmul2  8835  ltmul2  8902  lemul2  8903  ltmulgt11  8910  ltmulgt12  8911  gt0div  8916  ge0div  8917  ltmuldiv  8920  ltrec1  8934  lerec2  8935  ledivdiv  8936  ltdiv23  8938  lediv23  8939  suprleubex  9000  creur  9005  creui  9006  nn1suc  9028  nnrecl  9266  znnsub  9396  zgt0ge1  9403  zltlen  9423  nn0n0n1ge2b  9424  nn0le2is012  9427  btwnnz  9439  gtndiv  9440  prime  9444  eluz2  9626  indstr2  9702  negm  9708  nn01to3  9710  qapne  9732  qltlen  9733  qreccl  9735  irrmulap  9741  divlt1lt  9818  divle1le  9819  nnledivrp  9860  xnn0xadd0  9961  xltadd2  9971  xsubge0  9975  xlesubadd  9977  iccid  10019  elioc2  10030  elico2  10031  elicc2  10032  elfz2  10109  fzen  10137  fzsubel  10154  elfzp1  10166  fzpr  10171  fzrevral2  10200  fzrevral3  10201  nn0disj  10232  2ffzeq  10235  fzosplitsni  10330  fvinim0ffz  10336  ioo0  10368  ico0  10370  ioc0  10371  modq0  10440  negqmod0  10442  zmodidfzo  10464  frecuzrdgtcl  10523  nn0ennn  10544  nninfinf  10554  sq11  10723  nn0le2msqd  10830  nn0opth2d  10834  hashen  10895  zfz1isolem1  10951  zfz1iso  10952  csbwrdg  10983  wrdnval  10984  eqwrd  10994  2shfti  11015  cjap  11090  cnreim  11162  rexfiuz  11173  rexanuz2  11175  abs00ap  11246  absext  11247  sqabs  11266  abslt  11272  absle  11273  absdiflt  11276  absdifle  11277  lenegsq  11279  minmax  11414  ltmininf  11419  mingeb  11426  xrminmax  11449  xrmin1inf  11451  xrmin2inf  11452  xrltmininf  11454  xrlemininf  11455  clim  11465  clim0c  11470  climrecvg1n  11532  zsumdc  11568  fsum2dlemstep  11618  binomlem  11667  pwm1geoserap1  11692  zproddc  11763  efieq  11919  sin01bnd  11941  cos01bnd  11942  dvdsval2  11974  modm1div  11984  zdvdsdc  11996  modmulconst  12007  dvdsaddr  12021  dvdsabseq  12031  fzocongeq  12042  zeo3  12052  odd2np1  12057  oddp1d2  12074  zob  12075  oddm1d2  12076  nnoddm1d2  12094  divalgb  12109  divalgmod  12111  modremain  12113  bits0  12132  bitsp1e  12136  bitsp1o  12137  bitscmp  12142  bitsinv1lem  12145  gcdn0gt0  12172  bezoutlemstep  12191  dvdssq  12225  nn0seqcvgd  12236  algcvgblem  12244  lcmdvds  12274  lcmgcdeq  12278  coprmdvds  12287  qredeq  12291  congr  12295  isprm2  12312  isprm3  12313  prmdvdsexp  12343  prmdvdsexpb  12344  prmexpb  12346  prmfac1  12347  cncongrprm  12352  oddpwdclemxy  12364  oddpwdclemodd  12367  qnumdenbi  12387  qnumgt0  12393  hashdvds  12416  crth  12419  fermltl  12429  modprminveq  12446  pcpremul  12489  pc2dvds  12526  pcz  12528  prmpwdvds  12551  4sqlem16  12602  oddennn  12636  ctinfomlemom  12671  prdsbasmpt  12984  prdsbasmpt2  12992  mgm1  13074  ismhm  13165  mhmpropd  13170  issubm  13176  issubm2  13177  grpsubrcan  13285  grplactcnv  13306  grp1  13310  eqgval  13431  eqgid  13434  quselbasg  13438  isghm  13451  conjnmzb  13488  iscmn  13501  eqgabl  13538  rngmneg1  13581  rngmneg2  13582  rngpropd  13589  srgen1zr  13622  ringideu  13651  ringpropd  13672  crngpropd  13673  dvdsrd  13728  dvdsr02  13739  opprunitd  13744  crngunit  13745  unitpropdg  13782  rhmunitinv  13812  isnzr2  13818  issubrng  13833  resrhm2b  13883  aprval  13916  islmod  13925  islssm  13991  islssmg  13992  ellspsn  14051  isridl  14138  zrhrhmb  14256  zndvds  14283  znleval  14287  istopg  14321  eltg  14374  eltg2  14375  tgss2  14401  bastop1  14405  bastop2  14406  iscld  14425  isnei  14466  neiint  14467  iscn  14519  iscnp  14521  iscnp3  14525  tgcn  14530  ssidcn  14532  lmbr2  14536  lmbrf  14537  cnnei  14554  cnrest2  14558  eltx  14581  imasnopn  14621  ispsmet  14645  ismet  14666  isxmet  14667  metn0  14700  xmetres2  14701  elbl3ps  14716  elbl3  14717  xblpnfps  14720  xblpnf  14721  elmopn2  14771  metss  14816  bdxmet  14823  metrest  14828  xmetxp  14829  xmetxpbl  14830  metcnp3  14833  metcnp  14834  metcnp2  14835  metcn  14836  txmetcnp  14840  txmetcn  14841  metcnpd  14842  bl2ioo  14872  addcncntoplem  14883  elcncf  14895  elcncf2  14896  ivthdec  14966  ellimc3apf  14982  cnlimcim  14993  dveflem  15048  ply1termlem  15064  sincosq2sgn  15149  sinq12gt0  15152  logltb  15196  ltexp2  15263  wilthlem1  15302  lgsdilem  15354  lgsdir2lem4  15358  lgsdir2  15360  lgsne0  15365  lgsabs1  15366  gausslemma2dlem3  15390  gausslemma2dlem7  15395  lgseisenlem3  15399  lgsquad3  15411  2lgslem1a  15415  2lgslem3c  15422  2lgslem3d  15423  2lgsoddprmlem4  15439  2sqlem7  15448  2sqlem8a  15449  cbvrald  15520  bj-nalset  15627  bj-sels  15646  bj-nnelirr  15685  isomninnlem  15765  iswomninnlem  15784  iswomni0  15786  ismkvnnlem  15787