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  798  con1biidc  882  pm4.54dc  907  dn1dc  966  dedlem0a  974  dfifp3dc  988  dfifp4dc  989  dfifp5dc  990  3bior2fd  1388  xorbi12d  1424  nbbndc  1436  eleq12d  2300  neeq12d  2420  neleq12d  2501  raleqbi1dv  2740  rexeqbi1dv  2741  reueqd  2742  rmoeqd  2743  raleqbidv  2744  rexeqbidv  2745  raleqbidva  2746  rexeqbidva  2747  eueq3dc  2977  sbc19.21g  3097  sbcabel  3111  sbcel1g  3143  sbceq1g  3144  sbcel2g  3145  sbceq2g  3146  sbccsb2g  3154  sbcco3g  3182  sseq12d  3255  raaanlem  3596  sbcssg  3600  ralsng  3706  2ralunsn  3877  csbunig  3896  disjeq12d  4068  breq123d  4097  sbcbr12g  4139  sbcbr1g  4140  sbcbr2g  4141  treq  4188  nalset  4214  exmidsssn  4286  copsex4g  4333  onsucb  4595  posng  4791  csbxpg  4800  sbcrel  4805  csbcnvg  4906  eliniseg  5098  brcodir  5116  csbrng  5190  sbcfung  5342  fneq12d  5413  feq12d  5463  feq123d  5464  sbcfng  5471  sbcfg  5472  f1osng  5616  csbfv12g  5669  funimass4  5686  dmfco  5704  eqfnfv  5734  eqfnfv2  5735  fneqeql2  5746  fvimacnvi  5751  funimass3  5753  fniniseg  5757  rexsupp  5761  unpreima  5762  ralrnmpt  5779  rexrnmpt  5780  dffo3  5784  fmptco  5803  fressnfv  5830  eufnfv  5874  foima2  5881  fnunirn  5897  dff13  5898  f1elima  5903  cocan1  5917  cocan2  5918  fliftel  5923  fliftf  5929  isoresbr  5939  isoini  5948  f1oiso  5956  f1ofveu  5995  mpoeq123dva  6071  ovid  6127  ov  6130  ovg  6150  ovelrn  6160  caovord2d  6181  ofrfval2  6241  offveqb  6244  eqop  6329  reldm  6338  f1od2  6387  mpoxopoveq  6392  mpoxopovel  6393  tpostpos  6416  smoiso  6454  frecabcl  6551  frecsuclem  6558  nnaordr  6664  nnaword  6665  nnaordex  6682  ereq1  6695  brdifun  6715  erth2  6735  qliftfun  6772  brecop  6780  elmapg  6816  elpmg  6819  dom2lem  6931  xpcomco  6993  pw2f1odclem  7003  php5fin  7052  elfi2  7147  supisolem  7183  inflbti  7199  inl11  7240  ismkvnex  7330  mkvprop  7333  nninfwlporlemd  7347  exmidfodomrlemreseldju  7386  ltapig  7533  ltmpig  7534  nlt1pig  7536  mulcmpblnq  7563  ltsonq  7593  lt2addnq  7599  lt2mulnq  7600  archnqq  7612  prarloclemarch  7613  ltrnqg  7615  mulcmpblnq0  7639  preqlu  7667  genpdflem  7702  addnqprllem  7722  addnqprulem  7723  addlocprlemgt  7729  appdivnq  7758  mulnqprl  7763  mulnqpru  7764  mullocprlem  7765  distrlem4prl  7779  distrlem4pru  7780  1idprl  7785  1idpru  7786  ltexprlemloc  7802  cauappcvgprlemladdrl  7852  cauappcvgprlemladd  7853  cauappcvgprlem1  7854  archrecnq  7858  caucvgprlemnkj  7861  caucvgprprlemexb  7902  addcmpblnr  7934  lttrsr  7957  ltsosr  7959  ltasrg  7965  mulextsr1  7976  srpospr  7978  caucvgsrlemcau  7988  caucvgsrlemgt1  7990  caucvgsrlemoffres  7995  map2psrprg  8000  ltresr  8034  axcaucvglemres  8094  eqlelt  8241  cnegexlem1  8329  negeu  8345  subadd2  8358  subcan2  8379  addrsub  8525  ltaddneg  8579  ltaddnegr  8580  ltadd1  8584  leadd2  8586  ltsubadd  8587  lesubadd  8589  ltaddsub2  8592  leaddsub2  8594  ltaddpos  8607  lesub2  8612  ltsub2  8614  ltnegcon1  8618  ltnegcon2  8619  lenegcon1  8621  lenegcon2  8622  addge01  8627  addge02  8628  suble0  8631  leaddle0  8632  lesub0  8634  eqord2  8639  sublt0d  8725  recexre  8733  reaplt  8743  reapltxor  8744  reapneg  8752  remulext1  8754  apreim  8758  apcotr  8762  apadd2  8764  addext  8765  apsub1  8797  mulcanap2d  8817  diveqap0  8837  diveqap1  8860  apmul2  8944  ltmul2  9011  lemul2  9012  ltmulgt11  9019  ltmulgt12  9020  gt0div  9025  ge0div  9026  ltmuldiv  9029  ltrec1  9043  lerec2  9044  ledivdiv  9045  ltdiv23  9047  lediv23  9048  suprleubex  9109  creur  9114  creui  9115  nn1suc  9137  nnrecl  9375  znnsub  9506  zgt0ge1  9513  zltlen  9533  nn0n0n1ge2b  9534  nn0le2is012  9537  btwnnz  9549  gtndiv  9550  prime  9554  eluz2  9736  indstr2  9812  negm  9818  nn01to3  9820  qapne  9842  qltlen  9843  qreccl  9845  irrmulap  9851  divlt1lt  9928  divle1le  9929  nnledivrp  9970  xnn0xadd0  10071  xltadd2  10081  xsubge0  10085  xlesubadd  10087  iccid  10129  elioc2  10140  elico2  10141  elicc2  10142  elfz2  10219  fzen  10247  fzsubel  10264  elfzp1  10276  fzpr  10281  fzrevral2  10310  fzrevral3  10311  nn0disj  10342  2ffzeq  10345  fzosplitsni  10449  fvinim0ffz  10455  ioo0  10487  ico0  10489  ioc0  10490  modq0  10559  negqmod0  10561  zmodidfzo  10583  frecuzrdgtcl  10642  nn0ennn  10663  nninfinf  10673  sq11  10842  nn0le2msqd  10949  nn0opth2d  10953  hashen  11014  zfz1isolem1  11070  zfz1iso  11071  csbwrdg  11109  wrdnval  11110  eqwrd  11120  ccat0  11139  ccatws1lenp1bg  11176  swrd0g  11200  swrdspsleq  11207  pfxeq  11236  pfxsuffeqwrdeq  11238  pfxsuff1eqwrdeq  11239  ccatopth2  11257  wrd2ind  11263  2shfti  11350  cjap  11425  cnreim  11497  rexfiuz  11508  rexanuz2  11510  abs00ap  11581  absext  11582  sqabs  11601  abslt  11607  absle  11608  absdiflt  11611  absdifle  11612  lenegsq  11614  minmax  11749  ltmininf  11754  mingeb  11761  xrminmax  11784  xrmin1inf  11786  xrmin2inf  11787  xrltmininf  11789  xrlemininf  11790  clim  11800  clim0c  11805  climrecvg1n  11867  zsumdc  11903  fsum2dlemstep  11953  binomlem  12002  pwm1geoserap1  12027  zproddc  12098  efieq  12254  sin01bnd  12276  cos01bnd  12277  dvdsval2  12309  modm1div  12319  zdvdsdc  12331  modmulconst  12342  dvdsaddr  12356  dvdsabseq  12366  fzocongeq  12377  zeo3  12387  odd2np1  12392  oddp1d2  12409  zob  12410  oddm1d2  12411  nnoddm1d2  12429  divalgb  12444  divalgmod  12446  modremain  12448  bits0  12467  bitsp1e  12471  bitsp1o  12472  bitscmp  12477  bitsinv1lem  12480  gcdn0gt0  12507  bezoutlemstep  12526  dvdssq  12560  nn0seqcvgd  12571  algcvgblem  12579  lcmdvds  12609  lcmgcdeq  12613  coprmdvds  12622  qredeq  12626  congr  12630  isprm2  12647  isprm3  12648  prmdvdsexp  12678  prmdvdsexpb  12679  prmexpb  12681  prmfac1  12682  cncongrprm  12687  oddpwdclemxy  12699  oddpwdclemodd  12702  qnumdenbi  12722  qnumgt0  12728  hashdvds  12751  crth  12754  fermltl  12764  modprminveq  12781  pcpremul  12824  pc2dvds  12861  pcz  12863  prmpwdvds  12886  4sqlem16  12937  oddennn  12971  ctinfomlemom  13006  prdsbasmpt  13321  prdsbasmpt2  13329  mgm1  13411  ismhm  13502  mhmpropd  13507  issubm  13513  issubm2  13514  grpsubrcan  13622  grplactcnv  13643  grp1  13647  eqgval  13768  eqgid  13771  quselbasg  13775  isghm  13788  conjnmzb  13825  iscmn  13838  eqgabl  13875  rngmneg1  13918  rngmneg2  13919  rngpropd  13926  srgen1zr  13959  ringideu  13988  ringpropd  14009  crngpropd  14010  dvdsrd  14066  dvdsr02  14077  opprunitd  14082  crngunit  14083  unitpropdg  14120  rhmunitinv  14150  isnzr2  14156  issubrng  14171  resrhm2b  14221  aprval  14254  islmod  14263  islssm  14329  islssmg  14330  ellspsn  14389  isridl  14476  zrhrhmb  14594  zndvds  14621  znleval  14625  istopg  14681  eltg  14734  eltg2  14735  tgss2  14761  bastop1  14765  bastop2  14766  iscld  14785  isnei  14826  neiint  14827  iscn  14879  iscnp  14881  iscnp3  14885  tgcn  14890  ssidcn  14892  lmbr2  14896  lmbrf  14897  cnnei  14914  cnrest2  14918  eltx  14941  imasnopn  14981  ispsmet  15005  ismet  15026  isxmet  15027  metn0  15060  xmetres2  15061  elbl3ps  15076  elbl3  15077  xblpnfps  15080  xblpnf  15081  elmopn2  15131  metss  15176  bdxmet  15183  metrest  15188  xmetxp  15189  xmetxpbl  15190  metcnp3  15193  metcnp  15194  metcnp2  15195  metcn  15196  txmetcnp  15200  txmetcn  15201  metcnpd  15202  bl2ioo  15232  addcncntoplem  15243  elcncf  15255  elcncf2  15256  ivthdec  15326  ellimc3apf  15342  cnlimcim  15353  dveflem  15408  ply1termlem  15424  sincosq2sgn  15509  sinq12gt0  15512  logltb  15556  ltexp2  15623  wilthlem1  15662  lgsdilem  15714  lgsdir2lem4  15718  lgsdir2  15720  lgsne0  15725  lgsabs1  15726  gausslemma2dlem3  15750  gausslemma2dlem7  15755  lgseisenlem3  15759  lgsquad3  15771  2lgslem1a  15775  2lgslem3c  15782  2lgslem3d  15783  2lgsoddprmlem4  15799  2sqlem7  15808  2sqlem8a  15809  uhgreq12g  15884  isuhgropm  15889  uhgr0e  15890  upgrop  15912  uhgrvtxedgiedgb  15949  isuspgropen  15970  isusgropen  15971  uhgr2edg  16012  iswlk  16044  upgriswlkdc  16081  istrl  16104  cbvrald  16176  bj-nalset  16282  bj-sels  16301  bj-nnelirr  16340  isomninnlem  16428  iswomninnlem  16447  iswomni0  16449  ismkvnnlem  16450