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  801  con1biidc  885  pm4.54dc  910  dn1dc  969  dedlem0a  977  dfifp3dc  991  dfifp4dc  992  dfifp5dc  993  3bior2fd  1391  xorbi12d  1427  nbbndc  1439  eleq12d  2303  neeq12d  2432  neleq12d  2513  raleqbi1dv  2752  rexeqbi1dv  2753  reueqd  2754  rmoeqd  2755  raleqbidv  2756  rexeqbidv  2757  raleqbidva  2758  rexeqbidva  2759  eueq3dc  2990  sbc19.21g  3110  sbcabel  3124  sbcel1g  3156  sbceq1g  3157  sbcel2g  3158  sbceq2g  3159  sbccsb2g  3167  sbcco3g  3195  sseq12d  3268  raaanlem  3613  sbcssg  3617  ralsng  3728  2ralunsn  3902  csbunig  3921  disjeq12d  4093  breq123d  4122  sbcbr12g  4164  sbcbr1g  4165  sbcbr2g  4166  treq  4213  nalset  4239  exmidsssn  4314  copsex4g  4362  onsucb  4624  posng  4821  csbxpg  4830  sbcrel  4835  csbcnvg  4938  eliniseg  5131  brcodir  5149  csbrng  5223  sbcfung  5375  fneq12d  5447  feq12d  5497  feq123d  5498  sbcfng  5505  sbcfg  5506  f1osng  5656  csbfv12g  5709  funimass4  5726  dmfco  5744  eqfnfv  5774  eqfnfv2  5775  fneqeql2  5786  fvimacnvi  5791  funimass3  5793  fniniseg  5797  unpreima  5801  ralrnmpt  5818  rexrnmpt  5819  dffo3  5823  fmptco  5842  fressnfv  5870  eufnfv  5916  foima2  5923  fnunirn  5939  dff13  5940  f1elima  5945  cocan1  5959  cocan2  5960  fliftel  5965  fliftf  5971  isoresbr  5981  isoini  5990  f1oiso  5998  f1ofveu  6037  mpoeq123dva  6113  ovid  6169  ov  6172  ovg  6192  ovelrn  6202  caovord2d  6223  ofrfval2  6282  offveqb  6285  eqop  6370  reldm  6379  f1od2  6430  suppval1  6438  suppssrst  6460  suppssrgst  6461  mpoxopoveq  6470  mpoxopovel  6471  tpostpos  6494  smoiso  6532  frecabcl  6629  frecsuclem  6636  nnaordr  6742  nnaword  6743  nnaordex  6760  ereq1  6773  brdifun  6793  erth2  6813  qliftfun  6850  brecop  6858  elmapg  6894  elpmg  6897  mapsnd  6922  dom2lem  7010  xpcomco  7076  pw2f1odclem  7086  php5fin  7138  funisfsupp  7243  ffsuppbi  7252  elfi2  7258  supisolem  7298  inflbti  7314  inl11  7355  ismkvnex  7445  mkvprop  7448  nninfwlporlemd  7462  exmidfodomrlemreseldju  7502  ltapig  7649  ltmpig  7650  nlt1pig  7652  mulcmpblnq  7679  ltsonq  7709  lt2addnq  7715  lt2mulnq  7716  archnqq  7728  prarloclemarch  7729  ltrnqg  7731  mulcmpblnq0  7755  preqlu  7783  genpdflem  7818  addnqprllem  7838  addnqprulem  7839  addlocprlemgt  7845  appdivnq  7874  mulnqprl  7879  mulnqpru  7880  mullocprlem  7881  distrlem4prl  7895  distrlem4pru  7896  1idprl  7901  1idpru  7902  ltexprlemloc  7918  cauappcvgprlemladdrl  7968  cauappcvgprlemladd  7969  cauappcvgprlem1  7970  archrecnq  7974  caucvgprlemnkj  7977  caucvgprprlemexb  8018  addcmpblnr  8050  lttrsr  8073  ltsosr  8075  ltasrg  8081  mulextsr1  8092  srpospr  8094  caucvgsrlemcau  8104  caucvgsrlemgt1  8106  caucvgsrlemoffres  8111  map2psrprg  8116  ltresr  8150  axcaucvglemres  8210  eqlelt  8356  cnegexlem1  8444  negeu  8460  subadd2  8473  subcan2  8494  addrsub  8640  ltaddneg  8694  ltaddnegr  8695  ltadd1  8699  leadd2  8701  ltsubadd  8702  lesubadd  8704  ltaddsub2  8707  leaddsub2  8709  ltaddpos  8722  lesub2  8727  ltsub2  8729  ltnegcon1  8733  ltnegcon2  8734  lenegcon1  8736  lenegcon2  8737  addge01  8742  addge02  8743  suble0  8746  leaddle0  8747  lesub0  8749  eqord2  8754  sublt0d  8840  recexre  8848  reaplt  8858  reapltxor  8859  reapneg  8867  remulext1  8869  apreim  8873  apcotr  8877  apadd2  8879  addext  8880  apsub1  8912  mulcanap2d  8932  diveqap0  8952  diveqap1  8975  apmul2  9059  ltmul2  9126  lemul2  9127  ltmulgt11  9134  ltmulgt12  9135  gt0div  9140  ge0div  9141  ltmuldiv  9144  ltrec1  9158  lerec2  9159  ledivdiv  9160  ltdiv23  9162  lediv23  9163  suprleubex  9224  creur  9229  creui  9230  nn1suc  9252  nnrecl  9490  fcdmnn0fsuppg  9547  znnsub  9625  zgt0ge1  9632  zltlen  9652  nn0n0n1ge2b  9653  nn0le2is012  9656  btwnnz  9668  gtndiv  9669  prime  9673  eluz2  9855  indstr2  9937  negm  9943  nn01to3  9945  qapne  9967  qltlen  9968  qreccl  9970  irrmulap  9976  divlt1lt  10053  divle1le  10054  nnledivrp  10095  xnn0xadd0  10196  xltadd2  10206  xsubge0  10210  xlesubadd  10212  iccid  10254  elioc2  10265  elico2  10266  elicc2  10267  elfz2  10345  fzen  10373  fzsubel  10390  elfzp1  10402  fzpr  10407  fzrevral2  10436  fzrevral3  10437  nn0disj  10468  2ffzeq  10471  fzosplitsni  10577  fvinim0ffz  10583  ioo0  10615  ico0  10617  ioc0  10618  modq0  10687  negqmod0  10689  zmodidfzo  10711  frecuzrdgtcl  10770  nn0ennn  10791  nninfinf  10801  sq11  10970  nn0le2msqd  11077  nn0opth2d  11081  hashen  11142  zfz1isolem1  11205  zfz1iso  11206  csbwrdg  11247  wrdnval  11248  eqwrd  11258  ccat0  11277  ccatws1lenp1bg  11316  swrd0g  11345  swrdspsleq  11352  pfxeq  11381  pfxsuffeqwrdeq  11383  pfxsuff1eqwrdeq  11384  ccatopth2  11402  wrd2ind  11408  2shfti  11509  cjap  11584  cnreim  11656  rexfiuz  11667  rexanuz2  11669  abs00ap  11740  absext  11741  sqabs  11760  abslt  11766  absle  11767  absdiflt  11770  absdifle  11771  lenegsq  11773  minmax  11908  ltmininf  11913  mingeb  11920  xrminmax  11943  xrmin1inf  11945  xrmin2inf  11946  xrltmininf  11948  xrlemininf  11949  clim  11959  clim0c  11964  climrecvg1n  12026  zsumdc  12063  fsum2dlemstep  12113  binomlem  12162  pwm1geoserap1  12187  zproddc  12258  efieq  12414  sin01bnd  12436  cos01bnd  12437  dvdsval2  12469  modm1div  12479  zdvdsdc  12491  modmulconst  12502  dvdsaddr  12516  dvdsabseq  12526  fzocongeq  12537  zeo3  12547  odd2np1  12552  oddp1d2  12569  zob  12570  oddm1d2  12571  nnoddm1d2  12589  divalgb  12604  divalgmod  12606  modremain  12608  bits0  12627  bitsp1e  12631  bitsp1o  12632  bitscmp  12637  bitsinv1lem  12640  gcdn0gt0  12667  bezoutlemstep  12686  dvdssq  12720  nn0seqcvgd  12731  algcvgblem  12739  lcmdvds  12769  lcmgcdeq  12773  coprmdvds  12782  qredeq  12786  congr  12790  isprm2  12807  isprm3  12808  prmdvdsexp  12838  prmdvdsexpb  12839  prmexpb  12841  prmfac1  12842  cncongrprm  12847  oddpwdclemxy  12859  oddpwdclemodd  12862  qnumdenbi  12882  qnumgt0  12888  hashdvds  12911  crth  12914  fermltl  12924  modprminveq  12941  pcpremul  12984  pc2dvds  13021  pcz  13023  prmpwdvds  13046  4sqlem16  13097  oddennn  13132  ctinfomlemom  13167  prdsbasmpt  13482  prdsbasmpt2  13490  mgm1  13572  ismhm  13663  mhmpropd  13668  issubm  13674  issubm2  13675  grpsubrcan  13783  grplactcnv  13804  grp1  13808  eqgval  13929  eqgid  13932  quselbasg  13936  isghm  13949  conjnmzb  13986  iscmn  13999  eqgabl  14036  rngmneg1  14080  rngmneg2  14081  rngpropd  14088  srgen1zr  14121  ringideu  14150  ringpropd  14171  crngpropd  14172  dvdsrd  14228  dvdsr02  14239  opprunitd  14244  crngunit  14245  unitpropdg  14282  rhmunitinv  14312  isnzr2  14318  issubrng  14333  resrhm2b  14383  aprval  14417  islmod  14426  islssm  14492  islssmg  14493  ellspsn  14552  isridl  14639  zrhrhmb  14757  zndvds  14784  znleval  14788  istopg  14851  eltg  14904  eltg2  14905  tgss2  14931  bastop1  14935  bastop2  14936  iscld  14955  isnei  14996  neiint  14997  iscn  15049  iscnp  15051  iscnp3  15055  tgcn  15060  ssidcn  15062  lmbr2  15066  lmbrf  15067  cnnei  15084  cnrest2  15088  eltx  15111  imasnopn  15151  ispsmet  15175  ismet  15196  isxmet  15197  metn0  15230  xmetres2  15231  elbl3ps  15246  elbl3  15247  xblpnfps  15250  xblpnf  15251  elmopn2  15301  metss  15346  bdxmet  15353  metrest  15358  xmetxp  15359  xmetxpbl  15360  metcnp3  15363  metcnp  15364  metcnp2  15365  metcn  15366  txmetcnp  15370  txmetcn  15371  metcnpd  15372  bl2ioo  15402  addcncntoplem  15413  elcncf  15425  elcncf2  15426  ivthdec  15496  ellimc3apf  15512  cnlimcim  15523  dveflem  15578  ply1termlem  15594  sincosq2sgn  15679  sinq12gt0  15682  logltb  15726  ltexp2  15793  wilthlem1  15835  lgsdilem  15887  lgsdir2lem4  15891  lgsdir2  15893  lgsne0  15898  lgsabs1  15899  gausslemma2dlem3  15923  gausslemma2dlem7  15928  lgseisenlem3  15932  lgsquad3  15944  2lgslem1a  15948  2lgslem3c  15955  2lgslem3d  15956  2lgsoddprmlem4  15972  2sqlem7  15981  2sqlem8a  15982  uhgreq12g  16058  isuhgropm  16063  uhgr0e  16064  upgrop  16086  uhgrvtxedgiedgb  16125  isuspgropen  16146  isusgropen  16147  uhgr2edg  16188  issubgr2  16240  uhgrspansubgrlem  16258  vtxd0nedgbfi  16281  1loopgrvd0fi  16288  iswlk  16305  upgriswlkdc  16342  istrl  16367  iseupth  16429  eupth2lem2dc  16441  eupth2lem3lem3fi  16452  eupth2lem3lem4fi  16455  eupth2lem3lem7fi  16456  cbvrald  16547  bj-nalset  16652  bj-sels  16671  bj-nnelirr  16710  isomninnlem  16801  iswomninnlem  16821  iswomni0  16823  ismkvnnlem  16824