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  795  con1biidc  879  pm4.54dc  904  dn1dc  963  dedlem0a  971  3bior2fd  1366  xorbi12d  1402  nbbndc  1414  eleq12d  2277  neeq12d  2397  neleq12d  2478  raleqbi1dv  2715  rexeqbi1dv  2716  reueqd  2717  rmoeqd  2718  raleqbidv  2719  rexeqbidv  2720  raleqbidva  2721  rexeqbidva  2722  eueq3dc  2948  sbc19.21g  3068  sbcabel  3081  sbcel1g  3113  sbceq1g  3114  sbcel2g  3115  sbceq2g  3116  sbccsb2g  3124  sbcco3g  3152  sseq12d  3225  raaanlem  3566  sbcssg  3570  ralsng  3674  2ralunsn  3841  csbunig  3860  disjeq12d  4032  breq123d  4061  sbcbr12g  4103  sbcbr1g  4104  sbcbr2g  4105  treq  4152  nalset  4178  exmidsssn  4250  copsex4g  4295  onsucb  4555  posng  4751  csbxpg  4760  sbcrel  4765  csbcnvg  4866  eliniseg  5057  brcodir  5075  csbrng  5149  sbcfung  5300  fneq12d  5371  feq12d  5421  feq123d  5422  sbcfng  5429  sbcfg  5430  f1osng  5570  csbfv12g  5621  funimass4  5636  dmfco  5654  eqfnfv  5684  eqfnfv2  5685  fneqeql2  5696  fvimacnvi  5701  funimass3  5703  fniniseg  5707  rexsupp  5711  unpreima  5712  ralrnmpt  5729  rexrnmpt  5730  dffo3  5734  fmptco  5753  fressnfv  5778  eufnfv  5822  foima2  5827  fnunirn  5843  dff13  5844  f1elima  5849  cocan1  5863  cocan2  5864  fliftel  5869  fliftf  5875  isoresbr  5885  isoini  5894  f1oiso  5902  f1ofveu  5939  mpoeq123dva  6013  ovid  6069  ov  6072  ovg  6092  ovelrn  6102  caovord2d  6123  ofrfval2  6182  offveqb  6185  eqop  6270  reldm  6279  f1od2  6328  mpoxopoveq  6333  mpoxopovel  6334  tpostpos  6357  smoiso  6395  frecabcl  6492  frecsuclem  6499  nnaordr  6603  nnaword  6604  nnaordex  6621  ereq1  6634  brdifun  6654  erth2  6674  qliftfun  6711  brecop  6719  elmapg  6755  elpmg  6758  dom2lem  6870  xpcomco  6928  pw2f1odclem  6938  php5fin  6986  elfi2  7081  supisolem  7117  inflbti  7133  inl11  7174  ismkvnex  7264  mkvprop  7267  nninfwlporlemd  7281  exmidfodomrlemreseldju  7315  ltapig  7458  ltmpig  7459  nlt1pig  7461  mulcmpblnq  7488  ltsonq  7518  lt2addnq  7524  lt2mulnq  7525  archnqq  7537  prarloclemarch  7538  ltrnqg  7540  mulcmpblnq0  7564  preqlu  7592  genpdflem  7627  addnqprllem  7647  addnqprulem  7648  addlocprlemgt  7654  appdivnq  7683  mulnqprl  7688  mulnqpru  7689  mullocprlem  7690  distrlem4prl  7704  distrlem4pru  7705  1idprl  7710  1idpru  7711  ltexprlemloc  7727  cauappcvgprlemladdrl  7777  cauappcvgprlemladd  7778  cauappcvgprlem1  7779  archrecnq  7783  caucvgprlemnkj  7786  caucvgprprlemexb  7827  addcmpblnr  7859  lttrsr  7882  ltsosr  7884  ltasrg  7890  mulextsr1  7901  srpospr  7903  caucvgsrlemcau  7913  caucvgsrlemgt1  7915  caucvgsrlemoffres  7920  map2psrprg  7925  ltresr  7959  axcaucvglemres  8019  eqlelt  8166  cnegexlem1  8254  negeu  8270  subadd2  8283  subcan2  8304  addrsub  8450  ltaddneg  8504  ltaddnegr  8505  ltadd1  8509  leadd2  8511  ltsubadd  8512  lesubadd  8514  ltaddsub2  8517  leaddsub2  8519  ltaddpos  8532  lesub2  8537  ltsub2  8539  ltnegcon1  8543  ltnegcon2  8544  lenegcon1  8546  lenegcon2  8547  addge01  8552  addge02  8553  suble0  8556  leaddle0  8557  lesub0  8559  eqord2  8564  sublt0d  8650  recexre  8658  reaplt  8668  reapltxor  8669  reapneg  8677  remulext1  8679  apreim  8683  apcotr  8687  apadd2  8689  addext  8690  apsub1  8722  mulcanap2d  8742  diveqap0  8762  diveqap1  8785  apmul2  8869  ltmul2  8936  lemul2  8937  ltmulgt11  8944  ltmulgt12  8945  gt0div  8950  ge0div  8951  ltmuldiv  8954  ltrec1  8968  lerec2  8969  ledivdiv  8970  ltdiv23  8972  lediv23  8973  suprleubex  9034  creur  9039  creui  9040  nn1suc  9062  nnrecl  9300  znnsub  9431  zgt0ge1  9438  zltlen  9458  nn0n0n1ge2b  9459  nn0le2is012  9462  btwnnz  9474  gtndiv  9475  prime  9479  eluz2  9661  indstr2  9737  negm  9743  nn01to3  9745  qapne  9767  qltlen  9768  qreccl  9770  irrmulap  9776  divlt1lt  9853  divle1le  9854  nnledivrp  9895  xnn0xadd0  9996  xltadd2  10006  xsubge0  10010  xlesubadd  10012  iccid  10054  elioc2  10065  elico2  10066  elicc2  10067  elfz2  10144  fzen  10172  fzsubel  10189  elfzp1  10201  fzpr  10206  fzrevral2  10235  fzrevral3  10236  nn0disj  10267  2ffzeq  10270  fzosplitsni  10371  fvinim0ffz  10377  ioo0  10409  ico0  10411  ioc0  10412  modq0  10481  negqmod0  10483  zmodidfzo  10505  frecuzrdgtcl  10564  nn0ennn  10585  nninfinf  10595  sq11  10764  nn0le2msqd  10871  nn0opth2d  10875  hashen  10936  zfz1isolem1  10992  zfz1iso  10993  csbwrdg  11030  wrdnval  11031  eqwrd  11041  ccat0  11060  ccatws1lenp1bg  11097  swrd0g  11121  swrdspsleq  11128  pfxeq  11155  pfxsuffeqwrdeq  11157  pfxsuff1eqwrdeq  11158  2shfti  11186  cjap  11261  cnreim  11333  rexfiuz  11344  rexanuz2  11346  abs00ap  11417  absext  11418  sqabs  11437  abslt  11443  absle  11444  absdiflt  11447  absdifle  11448  lenegsq  11450  minmax  11585  ltmininf  11590  mingeb  11597  xrminmax  11620  xrmin1inf  11622  xrmin2inf  11623  xrltmininf  11625  xrlemininf  11626  clim  11636  clim0c  11641  climrecvg1n  11703  zsumdc  11739  fsum2dlemstep  11789  binomlem  11838  pwm1geoserap1  11863  zproddc  11934  efieq  12090  sin01bnd  12112  cos01bnd  12113  dvdsval2  12145  modm1div  12155  zdvdsdc  12167  modmulconst  12178  dvdsaddr  12192  dvdsabseq  12202  fzocongeq  12213  zeo3  12223  odd2np1  12228  oddp1d2  12245  zob  12246  oddm1d2  12247  nnoddm1d2  12265  divalgb  12280  divalgmod  12282  modremain  12284  bits0  12303  bitsp1e  12307  bitsp1o  12308  bitscmp  12313  bitsinv1lem  12316  gcdn0gt0  12343  bezoutlemstep  12362  dvdssq  12396  nn0seqcvgd  12407  algcvgblem  12415  lcmdvds  12445  lcmgcdeq  12449  coprmdvds  12458  qredeq  12462  congr  12466  isprm2  12483  isprm3  12484  prmdvdsexp  12514  prmdvdsexpb  12515  prmexpb  12517  prmfac1  12518  cncongrprm  12523  oddpwdclemxy  12535  oddpwdclemodd  12538  qnumdenbi  12558  qnumgt0  12564  hashdvds  12587  crth  12590  fermltl  12600  modprminveq  12617  pcpremul  12660  pc2dvds  12697  pcz  12699  prmpwdvds  12722  4sqlem16  12773  oddennn  12807  ctinfomlemom  12842  prdsbasmpt  13156  prdsbasmpt2  13164  mgm1  13246  ismhm  13337  mhmpropd  13342  issubm  13348  issubm2  13349  grpsubrcan  13457  grplactcnv  13478  grp1  13482  eqgval  13603  eqgid  13606  quselbasg  13610  isghm  13623  conjnmzb  13660  iscmn  13673  eqgabl  13710  rngmneg1  13753  rngmneg2  13754  rngpropd  13761  srgen1zr  13794  ringideu  13823  ringpropd  13844  crngpropd  13845  dvdsrd  13900  dvdsr02  13911  opprunitd  13916  crngunit  13917  unitpropdg  13954  rhmunitinv  13984  isnzr2  13990  issubrng  14005  resrhm2b  14055  aprval  14088  islmod  14097  islssm  14163  islssmg  14164  ellspsn  14223  isridl  14310  zrhrhmb  14428  zndvds  14455  znleval  14459  istopg  14515  eltg  14568  eltg2  14569  tgss2  14595  bastop1  14599  bastop2  14600  iscld  14619  isnei  14660  neiint  14661  iscn  14713  iscnp  14715  iscnp3  14719  tgcn  14724  ssidcn  14726  lmbr2  14730  lmbrf  14731  cnnei  14748  cnrest2  14752  eltx  14775  imasnopn  14815  ispsmet  14839  ismet  14860  isxmet  14861  metn0  14894  xmetres2  14895  elbl3ps  14910  elbl3  14911  xblpnfps  14914  xblpnf  14915  elmopn2  14965  metss  15010  bdxmet  15017  metrest  15022  xmetxp  15023  xmetxpbl  15024  metcnp3  15027  metcnp  15028  metcnp2  15029  metcn  15030  txmetcnp  15034  txmetcn  15035  metcnpd  15036  bl2ioo  15066  addcncntoplem  15077  elcncf  15089  elcncf2  15090  ivthdec  15160  ellimc3apf  15176  cnlimcim  15187  dveflem  15242  ply1termlem  15258  sincosq2sgn  15343  sinq12gt0  15346  logltb  15390  ltexp2  15457  wilthlem1  15496  lgsdilem  15548  lgsdir2lem4  15552  lgsdir2  15554  lgsne0  15559  lgsabs1  15560  gausslemma2dlem3  15584  gausslemma2dlem7  15589  lgseisenlem3  15593  lgsquad3  15605  2lgslem1a  15609  2lgslem3c  15616  2lgslem3d  15617  2lgsoddprmlem4  15633  2sqlem7  15642  2sqlem8a  15643  uhgreq12g  15716  isuhgropm  15721  uhgr0e  15722  cbvrald  15798  bj-nalset  15905  bj-sels  15924  bj-nnelirr  15963  isomninnlem  16043  iswomninnlem  16062  iswomni0  16064  ismkvnnlem  16065