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  793  con1biidc  877  pm4.54dc  902  dn1dc  960  dedlem0a  968  xorbi12d  1382  nbbndc  1394  eleq12d  2248  neeq12d  2367  neleq12d  2448  raleqbi1dv  2681  rexeqbi1dv  2682  reueqd  2683  rmoeqd  2684  raleqbidv  2685  rexeqbidv  2686  raleqbidva  2687  rexeqbidva  2688  eueq3dc  2913  sbc19.21g  3033  sbcabel  3046  sbcel1g  3078  sbceq1g  3079  sbcel2g  3080  sbceq2g  3081  sbccsb2g  3089  sbcco3g  3116  sseq12d  3188  raaanlem  3530  sbcssg  3534  ralsng  3634  2ralunsn  3800  csbunig  3819  disjeq12d  3991  breq123d  4019  sbcbr12g  4060  sbcbr1g  4061  sbcbr2g  4062  treq  4109  nalset  4135  exmidsssn  4204  copsex4g  4249  onsucb  4504  posng  4700  csbxpg  4709  sbcrel  4714  csbcnvg  4813  eliniseg  5000  brcodir  5018  csbrng  5092  sbcfung  5242  fneq12d  5310  feq12d  5357  feq123d  5358  sbcfng  5365  sbcfg  5366  f1osng  5504  csbfv12g  5553  funimass4  5568  dmfco  5586  eqfnfv  5615  eqfnfv2  5616  fneqeql2  5627  fvimacnvi  5632  funimass3  5634  fniniseg  5638  rexsupp  5642  unpreima  5643  ralrnmpt  5660  rexrnmpt  5661  dffo3  5665  fmptco  5684  fressnfv  5705  eufnfv  5749  foima2  5754  fnunirn  5770  dff13  5771  f1elima  5776  cocan1  5790  cocan2  5791  fliftel  5796  fliftf  5802  isoresbr  5812  isoini  5821  f1oiso  5829  f1ofveu  5865  mpoeq123dva  5938  ovid  5993  ov  5996  ovg  6015  ovelrn  6025  caovord2d  6046  ofrfval2  6101  offveqb  6104  eqop  6180  reldm  6189  f1od2  6238  mpoxopoveq  6243  mpoxopovel  6244  tpostpos  6267  smoiso  6305  frecabcl  6402  frecsuclem  6409  nnaordr  6513  nnaword  6514  nnaordex  6531  ereq1  6544  brdifun  6564  erth2  6582  qliftfun  6619  brecop  6627  elmapg  6663  elpmg  6666  dom2lem  6774  xpcomco  6828  php5fin  6884  elfi2  6973  supisolem  7009  inflbti  7025  inl11  7066  ismkvnex  7155  mkvprop  7158  nninfwlporlemd  7172  exmidfodomrlemreseldju  7201  ltapig  7339  ltmpig  7340  nlt1pig  7342  mulcmpblnq  7369  ltsonq  7399  lt2addnq  7405  lt2mulnq  7406  archnqq  7418  prarloclemarch  7419  ltrnqg  7421  mulcmpblnq0  7445  preqlu  7473  genpdflem  7508  addnqprllem  7528  addnqprulem  7529  addlocprlemgt  7535  appdivnq  7564  mulnqprl  7569  mulnqpru  7570  mullocprlem  7571  distrlem4prl  7585  distrlem4pru  7586  1idprl  7591  1idpru  7592  ltexprlemloc  7608  cauappcvgprlemladdrl  7658  cauappcvgprlemladd  7659  cauappcvgprlem1  7660  archrecnq  7664  caucvgprlemnkj  7667  caucvgprprlemexb  7708  addcmpblnr  7740  lttrsr  7763  ltsosr  7765  ltasrg  7771  mulextsr1  7782  srpospr  7784  caucvgsrlemcau  7794  caucvgsrlemgt1  7796  caucvgsrlemoffres  7801  map2psrprg  7806  ltresr  7840  axcaucvglemres  7900  eqlelt  8046  cnegexlem1  8134  negeu  8150  subadd2  8163  subcan2  8184  addrsub  8330  ltaddneg  8383  ltaddnegr  8384  ltadd1  8388  leadd2  8390  ltsubadd  8391  lesubadd  8393  ltaddsub2  8396  leaddsub2  8398  ltaddpos  8411  lesub2  8416  ltsub2  8418  ltnegcon1  8422  ltnegcon2  8423  lenegcon1  8425  lenegcon2  8426  addge01  8431  addge02  8432  suble0  8435  leaddle0  8436  lesub0  8438  eqord2  8443  sublt0d  8529  recexre  8537  reaplt  8547  reapltxor  8548  reapneg  8556  remulext1  8558  apreim  8562  apcotr  8566  apadd2  8568  addext  8569  apsub1  8601  mulcanap2d  8621  diveqap0  8641  diveqap1  8664  apmul2  8748  ltmul2  8815  lemul2  8816  ltmulgt11  8823  ltmulgt12  8824  gt0div  8829  ge0div  8830  ltmuldiv  8833  ltrec1  8847  lerec2  8848  ledivdiv  8849  ltdiv23  8851  lediv23  8852  suprleubex  8913  creur  8918  creui  8919  nn1suc  8940  nnrecl  9176  znnsub  9306  zgt0ge1  9313  zltlen  9333  nn0n0n1ge2b  9334  nn0le2is012  9337  btwnnz  9349  gtndiv  9350  prime  9354  eluz2  9536  indstr2  9611  negm  9617  nn01to3  9619  qapne  9641  qltlen  9642  qreccl  9644  divlt1lt  9726  divle1le  9727  nnledivrp  9768  xnn0xadd0  9869  xltadd2  9879  xsubge0  9883  xlesubadd  9885  iccid  9927  elioc2  9938  elico2  9939  elicc2  9940  elfz2  10017  fzen  10045  fzsubel  10062  elfzp1  10074  fzpr  10079  fzrevral2  10108  fzrevral3  10109  nn0disj  10140  2ffzeq  10143  fzosplitsni  10237  fvinim0ffz  10243  ioo0  10262  ico0  10264  ioc0  10265  modq0  10331  negqmod0  10333  zmodidfzo  10355  frecuzrdgtcl  10414  nn0ennn  10435  sq11  10595  nn0le2msqd  10701  nn0opth2d  10705  hashen  10766  zfz1isolem1  10822  zfz1iso  10823  2shfti  10842  cjap  10917  cnreim  10989  rexfiuz  11000  rexanuz2  11002  abs00ap  11073  absext  11074  sqabs  11093  abslt  11099  absle  11100  absdiflt  11103  absdifle  11104  lenegsq  11106  minmax  11240  ltmininf  11245  mingeb  11252  xrminmax  11275  xrmin1inf  11277  xrmin2inf  11278  xrltmininf  11280  xrlemininf  11281  clim  11291  clim0c  11296  climrecvg1n  11358  zsumdc  11394  fsum2dlemstep  11444  binomlem  11493  pwm1geoserap1  11518  zproddc  11589  efieq  11745  sin01bnd  11767  cos01bnd  11768  dvdsval2  11799  modm1div  11809  zdvdsdc  11821  modmulconst  11832  dvdsaddr  11846  dvdsabseq  11855  fzocongeq  11866  zeo3  11875  odd2np1  11880  oddp1d2  11897  zob  11898  oddm1d2  11899  nnoddm1d2  11917  divalgb  11932  divalgmod  11934  modremain  11936  gcdn0gt0  11981  bezoutlemstep  12000  dvdssq  12034  nn0seqcvgd  12043  algcvgblem  12051  lcmdvds  12081  lcmgcdeq  12085  coprmdvds  12094  qredeq  12098  congr  12102  isprm2  12119  isprm3  12120  prmdvdsexp  12150  prmdvdsexpb  12151  prmexpb  12153  prmfac1  12154  cncongrprm  12159  oddpwdclemxy  12171  oddpwdclemodd  12174  qnumdenbi  12194  qnumgt0  12200  hashdvds  12223  crth  12226  fermltl  12236  modprminveq  12252  pcpremul  12295  pc2dvds  12331  pcz  12333  prmpwdvds  12355  oddennn  12395  ctinfomlemom  12430  mgm1  12794  ismhm  12858  mhmpropd  12862  issubm  12868  issubm2  12869  grpsubrcan  12956  grplactcnv  12977  grp1  12981  eqgval  13087  eqgid  13090  iscmn  13101  srgen1zr  13176  ringideu  13205  ringpropd  13222  crngpropd  13223  dvdsrd  13268  dvdsr02  13279  opprunitd  13284  crngunit  13285  unitpropdg  13322  aprval  13377  islmod  13386  islssm  13450  istopg  13538  eltg  13591  eltg2  13592  tgss2  13618  bastop1  13622  bastop2  13623  iscld  13642  isnei  13683  neiint  13684  iscn  13736  iscnp  13738  iscnp3  13742  tgcn  13747  ssidcn  13749  lmbr2  13753  lmbrf  13754  cnnei  13771  cnrest2  13775  eltx  13798  imasnopn  13838  ispsmet  13862  ismet  13883  isxmet  13884  metn0  13917  xmetres2  13918  elbl3ps  13933  elbl3  13934  xblpnfps  13937  xblpnf  13938  elmopn2  13988  metss  14033  bdxmet  14040  metrest  14045  xmetxp  14046  xmetxpbl  14047  metcnp3  14050  metcnp  14051  metcnp2  14052  metcn  14053  txmetcnp  14057  txmetcn  14058  metcnpd  14059  bl2ioo  14081  addcncntoplem  14090  elcncf  14099  elcncf2  14100  ivthdec  14161  ellimc3apf  14168  cnlimcim  14179  dveflem  14226  sincosq2sgn  14287  sinq12gt0  14290  logltb  14334  ltexp2  14399  lgsdilem  14467  lgsdir2lem4  14471  lgsdir2  14473  lgsne0  14478  lgsabs1  14479  2lgsoddprmlem4  14499  2sqlem7  14507  2sqlem8a  14508  cbvrald  14579  bj-nalset  14686  bj-sels  14705  bj-nnelirr  14744  isomninnlem  14817  iswomninnlem  14836  iswomni0  14838  ismkvnnlem  14839