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  2305  neeq12d  2434  neleq12d  2515  raleqbi1dv  2755  rexeqbi1dv  2756  reueqd  2757  rmoeqd  2758  raleqbidv  2759  rexeqbidv  2760  raleqbidva  2761  rexeqbidva  2762  eueq3dc  2993  sbc19.21g  3113  sbcabel  3127  sbcel1g  3159  sbceq1g  3160  sbcel2g  3161  sbceq2g  3162  sbccsb2g  3170  sbcco3g  3198  sseq12d  3271  raaanlem  3616  sbcssg  3620  ralsng  3731  2ralunsn  3905  csbunig  3924  disjeq12d  4096  breq123d  4125  sbcbr12g  4167  sbcbr1g  4168  sbcbr2g  4169  treq  4216  nalset  4242  exmidsssn  4317  copsex4g  4365  onsucb  4627  posng  4824  csbxpg  4833  sbcrel  4838  csbcnvg  4941  eliniseg  5134  brcodir  5152  csbrng  5226  sbcfung  5378  fneq12d  5450  feq12d  5500  feq123d  5501  sbcfng  5508  sbcfg  5509  f1osng  5659  csbfv12g  5712  funimass4  5729  dmfco  5747  eqfnfv  5777  eqfnfv2  5778  fneqeql2  5789  fvimacnvi  5794  funimass3  5796  fniniseg  5800  unpreima  5804  ralrnmpt  5821  rexrnmpt  5822  dffo3  5826  fmptco  5845  fressnfv  5873  eufnfv  5919  foima2  5926  fnunirn  5942  dff13  5943  f1elima  5948  cocan1  5962  cocan2  5963  fliftel  5968  fliftf  5974  isoresbr  5984  isoini  5993  f1oiso  6001  f1ofveu  6040  mpoeq123dva  6116  ovid  6172  ov  6175  ovg  6195  ovelrn  6205  caovord2d  6226  ofrfval2  6285  offveqb  6288  eqop  6373  reldm  6382  f1od2  6433  suppval1  6441  suppssrst  6463  suppssrgst  6464  mpoxopoveq  6473  mpoxopovel  6474  tpostpos  6497  smoiso  6535  frecabcl  6632  frecsuclem  6639  nnaordr  6745  nnaword  6746  nnaordex  6763  ereq1  6776  brdifun  6796  erth2  6816  qliftfun  6853  brecop  6861  elmapg  6897  elpmg  6900  mapsnd  6925  dom2lem  7013  xpcomco  7079  pw2f1odclem  7089  php5fin  7141  funisfsupp  7246  ffsuppbi  7255  elfi2  7261  supisolem  7301  inflbti  7317  inl11  7358  ismkvnex  7448  mkvprop  7451  nninfwlporlemd  7465  exmidfodomrlemreseldju  7505  ltapig  7655  ltmpig  7656  nlt1pig  7658  mulcmpblnq  7685  ltsonq  7715  lt2addnq  7721  lt2mulnq  7722  archnqq  7734  prarloclemarch  7735  ltrnqg  7737  mulcmpblnq0  7761  preqlu  7789  genpdflem  7824  addnqprllem  7844  addnqprulem  7845  addlocprlemgt  7851  appdivnq  7880  mulnqprl  7885  mulnqpru  7886  mullocprlem  7887  distrlem4prl  7901  distrlem4pru  7902  1idprl  7907  1idpru  7908  ltexprlemloc  7924  cauappcvgprlemladdrl  7974  cauappcvgprlemladd  7975  cauappcvgprlem1  7976  archrecnq  7980  caucvgprlemnkj  7983  caucvgprprlemexb  8024  addcmpblnr  8056  lttrsr  8079  ltsosr  8081  ltasrg  8087  mulextsr1  8098  srpospr  8100  caucvgsrlemcau  8110  caucvgsrlemgt1  8112  caucvgsrlemoffres  8117  map2psrprg  8122  ltresr  8156  axcaucvglemres  8216  eqlelt  8362  cnegexlem1  8450  negeu  8466  subadd2  8479  subcan2  8500  addrsub  8646  ltaddneg  8700  ltaddnegr  8701  ltadd1  8705  leadd2  8707  ltsubadd  8708  lesubadd  8710  ltaddsub2  8713  leaddsub2  8715  ltaddpos  8728  lesub2  8733  ltsub2  8735  ltnegcon1  8739  ltnegcon2  8740  lenegcon1  8742  lenegcon2  8743  addge01  8748  addge02  8749  suble0  8752  leaddle0  8753  lesub0  8755  eqord2  8760  sublt0d  8846  recexre  8854  reaplt  8864  reapltxor  8865  reapneg  8873  remulext1  8875  apreim  8879  apcotr  8883  apadd2  8885  addext  8886  apsub1  8918  mulcanap2d  8938  diveqap0  8958  diveqap1  8981  apmul2  9065  ltmul2  9132  lemul2  9133  ltmulgt11  9140  ltmulgt12  9141  gt0div  9146  ge0div  9147  ltmuldiv  9150  ltrec1  9164  lerec2  9165  ledivdiv  9166  ltdiv23  9168  lediv23  9169  suprleubex  9230  creur  9235  creui  9236  nn1suc  9258  nnrecl  9496  fcdmnn0fsuppg  9553  znnsub  9631  zgt0ge1  9638  zltlen  9659  nn0n0n1ge2b  9660  nn0le2is012  9663  btwnnz  9675  gtndiv  9676  prime  9680  eluz2  9862  indstr2  9944  negm  9950  nn01to3  9952  qapne  9974  qltlen  9975  qreccl  9977  irrmulap  9983  divlt1lt  10060  divle1le  10061  nnledivrp  10102  xnn0xadd0  10203  xltadd2  10213  xsubge0  10217  xlesubadd  10219  iccid  10261  elioc2  10272  elico2  10273  elicc2  10274  elfz2  10352  fzen  10380  fzsubel  10397  elfzp1  10410  fzpr  10415  fzrevral2  10444  fzrevral3  10445  nn0disj  10476  2ffzeq  10479  fzosplitsni  10585  fvinim0ffz  10591  ioo0  10623  ico0  10625  ioc0  10626  modq0  10695  negqmod0  10697  zmodidfzo  10719  frecuzrdgtcl  10778  nn0ennn  10799  nninfinf  10809  sq11  10978  nn0le2msqd  11085  nn0opth2d  11089  hashen  11151  zfz1isolem1  11216  zfz1iso  11217  csbwrdg  11258  wrdnval  11259  eqwrd  11269  ccat0  11288  ccatws1lenp1bg  11327  swrd0g  11356  swrdspsleq  11363  pfxeq  11392  pfxsuffeqwrdeq  11394  pfxsuff1eqwrdeq  11395  ccatopth2  11413  wrd2ind  11419  2shfti  11520  cjap  11595  cnreim  11667  rexfiuz  11678  rexanuz2  11680  abs00ap  11751  absext  11752  sqabs  11771  abslt  11777  absle  11778  absdiflt  11781  absdifle  11782  lenegsq  11784  minmax  11919  ltmininf  11924  mingeb  11931  xrminmax  11954  xrmin1inf  11956  xrmin2inf  11957  xrltmininf  11959  xrlemininf  11960  clim  11970  clim0c  11975  climrecvg1n  12037  zsumdc  12074  fsum2dlemstep  12124  binomlem  12173  pwm1geoserap1  12198  zproddc  12269  efieq  12425  sin01bnd  12447  cos01bnd  12448  dvdsval2  12480  modm1div  12490  zdvdsdc  12502  modmulconst  12513  dvdsaddr  12527  dvdsabseq  12537  fzocongeq  12548  zeo3  12558  odd2np1  12563  oddp1d2  12580  zob  12581  oddm1d2  12582  nnoddm1d2  12600  divalgb  12615  divalgmod  12617  modremain  12619  bits0  12638  bitsp1e  12642  bitsp1o  12643  bitscmp  12648  bitsinv1lem  12651  gcdn0gt0  12678  bezoutlemstep  12697  dvdssq  12731  nn0seqcvgd  12742  algcvgblem  12750  lcmdvds  12780  lcmgcdeq  12784  coprmdvds  12793  qredeq  12797  congr  12801  isprm2  12818  isprm3  12819  prmdvdsexp  12849  prmdvdsexpb  12850  prmexpb  12852  prmfac1  12853  cncongrprm  12858  oddpwdclemxy  12870  oddpwdclemodd  12873  qnumdenbi  12893  qnumgt0  12899  hashdvds  12922  crth  12925  fermltl  12935  modprminveq  12952  pcpremul  12995  pc2dvds  13032  pcz  13034  prmpwdvds  13057  4sqlem16  13108  ballotfilemfc0  13153  ballotfilemfcc  13154  ballotfilemodife  13158  oddennn  13160  ctinfomlemom  13195  prdsbasmpt  13510  prdsbasmpt2  13518  mgm1  13600  ismhm  13691  mhmpropd  13696  issubm  13702  issubm2  13703  grpsubrcan  13811  grplactcnv  13832  grp1  13836  eqgval  13957  eqgid  13960  quselbasg  13964  isghm  13977  conjnmzb  14014  iscmn  14027  eqgabl  14064  rngmneg1  14108  rngmneg2  14109  rngpropd  14116  srgen1zr  14149  ringideu  14178  ringpropd  14199  crngpropd  14200  dvdsrd  14256  dvdsr02  14267  opprunitd  14272  crngunit  14273  unitpropdg  14310  rhmunitinv  14340  isnzr2  14346  issubrng  14361  resrhm2b  14411  aprval  14445  islmod  14456  islssm  14522  islssmg  14523  ellspsn  14582  isridl  14669  zrhrhmb  14787  zndvds  14814  znleval  14818  istopg  14881  eltg  14934  eltg2  14935  tgss2  14961  bastop1  14965  bastop2  14966  iscld  14985  isnei  15026  neiint  15027  iscn  15079  iscnp  15081  iscnp3  15085  tgcn  15090  ssidcn  15092  lmbr2  15096  lmbrf  15097  cnnei  15114  cnrest2  15118  eltx  15141  imasnopn  15181  ispsmet  15205  ismet  15226  isxmet  15227  metn0  15260  xmetres2  15261  elbl3ps  15276  elbl3  15277  xblpnfps  15280  xblpnf  15281  elmopn2  15331  metss  15376  bdxmet  15383  metrest  15388  xmetxp  15389  xmetxpbl  15390  metcnp3  15393  metcnp  15394  metcnp2  15395  metcn  15396  txmetcnp  15400  txmetcn  15401  metcnpd  15402  bl2ioo  15432  addcncntoplem  15443  elcncf  15455  elcncf2  15456  ivthdec  15526  ellimc3apf  15542  cnlimcim  15553  dveflem  15608  ply1termlem  15624  sincosq2sgn  15709  sinq12gt0  15712  logltb  15756  ltexp2  15823  wilthlem1  15865  lgsdilem  15917  lgsdir2lem4  15921  lgsdir2  15923  lgsne0  15928  lgsabs1  15929  gausslemma2dlem3  15953  gausslemma2dlem7  15958  lgseisenlem3  15962  lgsquad3  15974  2lgslem1a  15978  2lgslem3c  15985  2lgslem3d  15986  2lgsoddprmlem4  16002  2sqlem7  16011  2sqlem8a  16012  uhgreq12g  16088  isuhgropm  16093  uhgr0e  16094  upgrop  16116  uhgrvtxedgiedgb  16155  isuspgropen  16176  isusgropen  16177  uhgr2edg  16218  issubgr2  16270  uhgrspansubgrlem  16288  vtxd0nedgbfi  16311  1loopgrvd0fi  16318  iswlk  16335  upgriswlkdc  16372  istrl  16397  iseupth  16459  eupth2lem2dc  16471  eupth2lem3lem3fi  16482  eupth2lem3lem4fi  16485  eupth2lem3lem7fi  16486  cbvrald  16577  bj-nalset  16682  bj-sels  16701  bj-nnelirr  16740  isomninnlem  16831  iswomninnlem  16851  iswomni0  16853  ismkvnnlem  16854