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  2264  neeq12d  2384  neleq12d  2465  raleqbi1dv  2702  rexeqbi1dv  2703  reueqd  2704  rmoeqd  2705  raleqbidv  2706  rexeqbidv  2707  raleqbidva  2708  rexeqbidva  2709  eueq3dc  2935  sbc19.21g  3055  sbcabel  3068  sbcel1g  3100  sbceq1g  3101  sbcel2g  3102  sbceq2g  3103  sbccsb2g  3111  sbcco3g  3139  sseq12d  3211  raaanlem  3552  sbcssg  3556  ralsng  3659  2ralunsn  3825  csbunig  3844  disjeq12d  4016  breq123d  4044  sbcbr12g  4085  sbcbr1g  4086  sbcbr2g  4087  treq  4134  nalset  4160  exmidsssn  4232  copsex4g  4277  onsucb  4536  posng  4732  csbxpg  4741  sbcrel  4746  csbcnvg  4847  eliniseg  5036  brcodir  5054  csbrng  5128  sbcfung  5279  fneq12d  5347  feq12d  5394  feq123d  5395  sbcfng  5402  sbcfg  5403  f1osng  5542  csbfv12g  5593  funimass4  5608  dmfco  5626  eqfnfv  5656  eqfnfv2  5657  fneqeql2  5668  fvimacnvi  5673  funimass3  5675  fniniseg  5679  rexsupp  5683  unpreima  5684  ralrnmpt  5701  rexrnmpt  5702  dffo3  5706  fmptco  5725  fressnfv  5746  eufnfv  5790  foima2  5795  fnunirn  5811  dff13  5812  f1elima  5817  cocan1  5831  cocan2  5832  fliftel  5837  fliftf  5843  isoresbr  5853  isoini  5862  f1oiso  5870  f1ofveu  5907  mpoeq123dva  5980  ovid  6036  ov  6039  ovg  6059  ovelrn  6069  caovord2d  6090  ofrfval2  6149  offveqb  6152  eqop  6232  reldm  6241  f1od2  6290  mpoxopoveq  6295  mpoxopovel  6296  tpostpos  6319  smoiso  6357  frecabcl  6454  frecsuclem  6461  nnaordr  6565  nnaword  6566  nnaordex  6583  ereq1  6596  brdifun  6616  erth2  6636  qliftfun  6673  brecop  6681  elmapg  6717  elpmg  6720  dom2lem  6828  xpcomco  6882  pw2f1odclem  6892  php5fin  6940  elfi2  7033  supisolem  7069  inflbti  7085  inl11  7126  ismkvnex  7216  mkvprop  7219  nninfwlporlemd  7233  exmidfodomrlemreseldju  7262  ltapig  7400  ltmpig  7401  nlt1pig  7403  mulcmpblnq  7430  ltsonq  7460  lt2addnq  7466  lt2mulnq  7467  archnqq  7479  prarloclemarch  7480  ltrnqg  7482  mulcmpblnq0  7506  preqlu  7534  genpdflem  7569  addnqprllem  7589  addnqprulem  7590  addlocprlemgt  7596  appdivnq  7625  mulnqprl  7630  mulnqpru  7631  mullocprlem  7632  distrlem4prl  7646  distrlem4pru  7647  1idprl  7652  1idpru  7653  ltexprlemloc  7669  cauappcvgprlemladdrl  7719  cauappcvgprlemladd  7720  cauappcvgprlem1  7721  archrecnq  7725  caucvgprlemnkj  7728  caucvgprprlemexb  7769  addcmpblnr  7801  lttrsr  7824  ltsosr  7826  ltasrg  7832  mulextsr1  7843  srpospr  7845  caucvgsrlemcau  7855  caucvgsrlemgt1  7857  caucvgsrlemoffres  7862  map2psrprg  7867  ltresr  7901  axcaucvglemres  7961  eqlelt  8108  cnegexlem1  8196  negeu  8212  subadd2  8225  subcan2  8246  addrsub  8392  ltaddneg  8445  ltaddnegr  8446  ltadd1  8450  leadd2  8452  ltsubadd  8453  lesubadd  8455  ltaddsub2  8458  leaddsub2  8460  ltaddpos  8473  lesub2  8478  ltsub2  8480  ltnegcon1  8484  ltnegcon2  8485  lenegcon1  8487  lenegcon2  8488  addge01  8493  addge02  8494  suble0  8497  leaddle0  8498  lesub0  8500  eqord2  8505  sublt0d  8591  recexre  8599  reaplt  8609  reapltxor  8610  reapneg  8618  remulext1  8620  apreim  8624  apcotr  8628  apadd2  8630  addext  8631  apsub1  8663  mulcanap2d  8683  diveqap0  8703  diveqap1  8726  apmul2  8810  ltmul2  8877  lemul2  8878  ltmulgt11  8885  ltmulgt12  8886  gt0div  8891  ge0div  8892  ltmuldiv  8895  ltrec1  8909  lerec2  8910  ledivdiv  8911  ltdiv23  8913  lediv23  8914  suprleubex  8975  creur  8980  creui  8981  nn1suc  9003  nnrecl  9241  znnsub  9371  zgt0ge1  9378  zltlen  9398  nn0n0n1ge2b  9399  nn0le2is012  9402  btwnnz  9414  gtndiv  9415  prime  9419  eluz2  9601  indstr2  9677  negm  9683  nn01to3  9685  qapne  9707  qltlen  9708  qreccl  9710  irrmulap  9716  divlt1lt  9793  divle1le  9794  nnledivrp  9835  xnn0xadd0  9936  xltadd2  9946  xsubge0  9950  xlesubadd  9952  iccid  9994  elioc2  10005  elico2  10006  elicc2  10007  elfz2  10084  fzen  10112  fzsubel  10129  elfzp1  10141  fzpr  10146  fzrevral2  10175  fzrevral3  10176  nn0disj  10207  2ffzeq  10210  fzosplitsni  10305  fvinim0ffz  10311  ioo0  10331  ico0  10333  ioc0  10334  modq0  10403  negqmod0  10405  zmodidfzo  10427  frecuzrdgtcl  10486  nn0ennn  10507  nninfinf  10517  sq11  10686  nn0le2msqd  10793  nn0opth2d  10797  hashen  10858  zfz1isolem1  10914  zfz1iso  10915  csbwrdg  10946  wrdnval  10947  eqwrd  10957  2shfti  10978  cjap  11053  cnreim  11125  rexfiuz  11136  rexanuz2  11138  abs00ap  11209  absext  11210  sqabs  11229  abslt  11235  absle  11236  absdiflt  11239  absdifle  11240  lenegsq  11242  minmax  11376  ltmininf  11381  mingeb  11388  xrminmax  11411  xrmin1inf  11413  xrmin2inf  11414  xrltmininf  11416  xrlemininf  11417  clim  11427  clim0c  11432  climrecvg1n  11494  zsumdc  11530  fsum2dlemstep  11580  binomlem  11629  pwm1geoserap1  11654  zproddc  11725  efieq  11881  sin01bnd  11903  cos01bnd  11904  dvdsval2  11936  modm1div  11946  zdvdsdc  11958  modmulconst  11969  dvdsaddr  11983  dvdsabseq  11992  fzocongeq  12003  zeo3  12012  odd2np1  12017  oddp1d2  12034  zob  12035  oddm1d2  12036  nnoddm1d2  12054  divalgb  12069  divalgmod  12071  modremain  12073  gcdn0gt0  12118  bezoutlemstep  12137  dvdssq  12171  nn0seqcvgd  12182  algcvgblem  12190  lcmdvds  12220  lcmgcdeq  12224  coprmdvds  12233  qredeq  12237  congr  12241  isprm2  12258  isprm3  12259  prmdvdsexp  12289  prmdvdsexpb  12290  prmexpb  12292  prmfac1  12293  cncongrprm  12298  oddpwdclemxy  12310  oddpwdclemodd  12313  qnumdenbi  12333  qnumgt0  12339  hashdvds  12362  crth  12365  fermltl  12375  modprminveq  12391  pcpremul  12434  pc2dvds  12471  pcz  12473  prmpwdvds  12496  4sqlem16  12547  oddennn  12552  ctinfomlemom  12587  mgm1  12956  ismhm  13036  mhmpropd  13041  issubm  13047  issubm2  13048  grpsubrcan  13156  grplactcnv  13177  grp1  13181  eqgval  13296  eqgid  13299  quselbasg  13303  isghm  13316  conjnmzb  13353  iscmn  13366  eqgabl  13403  rngmneg1  13446  rngmneg2  13447  rngpropd  13454  srgen1zr  13487  ringideu  13516  ringpropd  13537  crngpropd  13538  dvdsrd  13593  dvdsr02  13604  opprunitd  13609  crngunit  13610  unitpropdg  13647  rhmunitinv  13677  isnzr2  13683  issubrng  13698  resrhm2b  13748  aprval  13781  islmod  13790  islssm  13856  islssmg  13857  ellspsn  13916  isridl  14003  zrhrhmb  14121  zndvds  14148  znleval  14152  istopg  14178  eltg  14231  eltg2  14232  tgss2  14258  bastop1  14262  bastop2  14263  iscld  14282  isnei  14323  neiint  14324  iscn  14376  iscnp  14378  iscnp3  14382  tgcn  14387  ssidcn  14389  lmbr2  14393  lmbrf  14394  cnnei  14411  cnrest2  14415  eltx  14438  imasnopn  14478  ispsmet  14502  ismet  14523  isxmet  14524  metn0  14557  xmetres2  14558  elbl3ps  14573  elbl3  14574  xblpnfps  14577  xblpnf  14578  elmopn2  14628  metss  14673  bdxmet  14680  metrest  14685  xmetxp  14686  xmetxpbl  14687  metcnp3  14690  metcnp  14691  metcnp2  14692  metcn  14693  txmetcnp  14697  txmetcn  14698  metcnpd  14699  bl2ioo  14729  addcncntoplem  14740  elcncf  14752  elcncf2  14753  ivthdec  14823  ellimc3apf  14839  cnlimcim  14850  dveflem  14905  ply1termlem  14921  sincosq2sgn  15003  sinq12gt0  15006  logltb  15050  ltexp2  15115  wilthlem1  15153  lgsdilem  15184  lgsdir2lem4  15188  lgsdir2  15190  lgsne0  15195  lgsabs1  15196  gausslemma2dlem3  15220  gausslemma2dlem7  15225  lgseisenlem3  15229  lgsquad3  15241  2lgslem1a  15245  2lgslem3c  15252  2lgslem3d  15253  2lgsoddprmlem4  15269  2sqlem7  15278  2sqlem8a  15279  cbvrald  15350  bj-nalset  15457  bj-sels  15476  bj-nnelirr  15515  isomninnlem  15590  iswomninnlem  15609  iswomni0  15611  ismkvnnlem  15612