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  466  anbi12d  477  orbi12d  805  con1biidc  889  pm4.54dc  914  dn1dc  973  dedlem0a  981  dfifp3dc  995  dfifp4dc  996  dfifp5dc  997  3bior2fd  1395  xorbi12d  1431  nbbndc  1443  eleq12d  2309  neeq12d  2440  neleq12d  2521  raleqbi1dv  2761  rexeqbi1dv  2762  reueqd  2763  rmoeqd  2764  raleqbidv  2765  rexeqbidv  2766  raleqbidva  2767  rexeqbidva  2768  eueq3dc  3000  sbc19.21g  3120  sbcabel  3134  sbcel1g  3166  sbceq1g  3167  sbcel2g  3168  sbceq2g  3169  sbccsb2g  3177  sbcco3g  3205  sseq12d  3279  raaanlem  3632  sbcssg  3636  ralsng  3748  2ralunsn  3922  csbunig  3941  disjeq12d  4113  breq123d  4142  sbcbr12g  4184  sbcbr1g  4185  sbcbr2g  4186  treq  4233  nalset  4261  exmidsssn  4337  copsex4g  4385  onsucb  4648  posng  4845  csbxpg  4854  sbcrel  4859  csbcnvg  4962  eliniseg  5155  brcodir  5173  csbrng  5247  sbcfung  5399  fneq12d  5471  feq12d  5521  feq123d  5522  sbcfng  5529  sbcfg  5530  f1osng  5680  csbfv12g  5733  funimass4  5750  dmfco  5770  eqfnfv  5800  eqfnfv2  5801  fneqeql2  5812  fvimacnvi  5817  funimass3  5819  fniniseg  5823  unpreima  5827  ralrnmpt  5844  rexrnmpt  5845  dffo3  5849  fmptco  5868  fressnfv  5896  eufnfv  5943  foima2  5951  fnunirn  5967  dff13  5968  f1elima  5973  cocan1  5987  cocan2  5988  fliftel  5993  fliftf  5999  isoresbr  6009  isoini  6018  f1oiso  6026  f1ofveu  6067  mpoeq123dva  6143  ovid  6199  ov  6202  ovg  6222  ovelrn  6232  caovord2d  6253  ofrfval2  6313  offveqb  6316  eqop  6405  reldm  6414  f1od2  6465  suppval1  6473  suppssrst  6495  suppssrgst  6496  mpoxopoveq  6505  mpoxopovel  6506  tpostpos  6529  smoiso  6567  frecabcl  6664  frecsuclem  6671  nnaordr  6777  nnaword  6778  nnaordex  6795  ereq1  6808  brdifun  6828  erth2  6848  qliftfun  6885  brecop  6893  elmapg  6929  elpmg  6932  mapsnd  6964  dom2lem  7052  xpcomco  7118  pw2f1odclem  7128  php5fin  7180  funisfsupp  7285  ffsuppbi  7294  elfi2  7300  supisolem  7342  inflbti  7358  inl11  7399  ismkvnex  7489  mkvprop  7492  nninfwlporlemd  7506  exmidfodomrlemreseldju  7546  ltapig  7699  ltmpig  7700  nlt1pig  7702  mulcmpblnq  7729  ltsonq  7759  lt2addnq  7765  lt2mulnq  7766  archnqq  7778  prarloclemarch  7779  ltrnqg  7781  mulcmpblnq0  7805  preqlu  7833  genpdflem  7868  addnqprllem  7888  addnqprulem  7889  addlocprlemgt  7895  appdivnq  7924  mulnqprl  7929  mulnqpru  7930  mullocprlem  7931  distrlem4prl  7945  distrlem4pru  7946  1idprl  7951  1idpru  7952  ltexprlemloc  7968  cauappcvgprlemladdrl  8018  cauappcvgprlemladd  8019  cauappcvgprlem1  8020  archrecnq  8024  caucvgprlemnkj  8027  caucvgprprlemexb  8068  addcmpblnr  8100  lttrsr  8123  ltsosr  8125  ltasrg  8131  mulextsr1  8142  srpospr  8144  caucvgsrlemcau  8154  caucvgsrlemgt1  8156  caucvgsrlemoffres  8161  map2psrprg  8166  ltresr  8200  axcaucvglemres  8260  eqlelt  8406  cnegexlem1  8495  negeu  8511  subadd2  8524  subcan2  8545  addrsub  8691  ltaddneg  8746  ltaddnegr  8747  ltadd1  8751  leadd2  8753  ltsubadd  8754  lesubadd  8756  ltaddsub2  8759  leaddsub2  8761  ltaddpos  8774  lesub2  8779  ltsub2  8781  ltnegcon1  8785  ltnegcon2  8786  lenegcon1  8788  lenegcon2  8789  addge01  8794  addge02  8795  suble0  8798  leaddle0  8799  lesub0  8801  eqord2  8806  sublt0d  8892  recexre  8900  reaplt  8910  reapltxor  8911  reapneg  8919  remulext1  8921  apreim  8925  apcotr  8929  apadd2  8931  addext  8932  apsub1  8964  mulcanap2d  8984  diveqap0  9006  diveqap1  9029  apmul2  9113  ltmul2  9180  lemul2  9181  ltmulgt11  9188  ltmulgt12  9189  gt0div  9194  ge0div  9195  ltmuldiv  9198  ltrec1  9212  lerec2  9213  ledivdiv  9214  ltdiv23  9216  lediv23  9217  suprleubex  9278  creur  9283  creui  9284  nn1suc  9306  nnrecl  9544  fcdmnn0fsuppg  9601  znnsub  9679  zgt0ge1  9686  zltlen  9707  nn0n0n1ge2b  9708  nn0le2is012  9711  btwnnz  9723  gtndiv  9724  prime  9728  eluz2  9910  indstr2  9992  negm  9998  nn01to3  10000  qapne  10022  qltlen  10023  qreccl  10025  irrmulap  10031  divlt1lt  10108  divle1le  10109  nnledivrp  10150  xnn0xadd0  10252  xltadd2  10262  xsubge0  10266  xlesubadd  10268  iccid  10310  elioc2  10321  elico2  10322  elicc2  10323  elfz2  10401  fzen  10430  fzsubel  10449  elfzp1  10462  fzpr  10467  fzrevral2  10496  fzrevral3  10497  nn0disj  10528  2ffzeq  10531  fzosplitsni  10637  fvinim0ffz  10643  ioo0  10677  ico0  10679  ioc0  10680  modq0  10749  negqmod0  10751  zmodidfzo  10773  frecuzrdgtcl  10832  nn0ennn  10853  nninfinf  10863  sq11  11032  nn0le2msqd  11140  nn0opth2d  11144  hashen  11206  zfz1isolem1  11275  zfz1iso  11276  csbwrdg  11317  wrdnval  11318  eqwrd  11328  ccat0  11347  ccatws1lenp1bg  11386  swrd0g  11415  swrdspsleq  11422  pfxeq  11451  pfxsuffeqwrdeq  11453  pfxsuff1eqwrdeq  11454  ccatopth2  11472  wrd2ind  11478  2shfti  11579  cjap  11655  cnreim  11727  rexfiuz  11738  rexanuz2  11740  abs00ap  11811  absext  11812  sqabs  11831  abslt  11837  absle  11838  absdiflt  11841  absdifle  11842  lenegsq  11844  minmax  11979  ltmininf  11984  mingeb  11991  xrminmax  12014  xrmin1inf  12016  xrmin2inf  12017  xrltmininf  12019  xrlemininf  12020  clim  12030  clim0c  12035  climrecvg1n  12097  zsumdc  12134  fsum2dlemstep  12184  binomlem  12233  pwm1geoserap1  12258  zproddc  12329  efieq  12485  sin01bnd  12507  cos01bnd  12508  dvdsval2  12540  modm1div  12550  zdvdsdc  12562  modmulconst  12573  dvdsaddr  12587  dvdsabseq  12597  fzocongeq  12608  zeo3  12618  odd2np1  12623  oddp1d2  12640  zob  12641  oddm1d2  12642  nnoddm1d2  12660  divalgb  12675  divalgmod  12677  modremain  12679  bits0  12698  bitsp1e  12702  bitsp1o  12703  bitscmp  12708  bitsinv1lem  12711  gcdn0gt0  12738  bezoutlemstep  12757  dvdssq  12791  nn0seqcvgd  12802  algcvgblem  12810  lcmdvds  12840  lcmgcdeq  12844  coprmdvds  12853  qredeq  12857  congr  12861  isprm2  12878  isprm3  12879  prmdvdsexp  12909  prmdvdsexpb  12910  prmexpb  12912  prmfac1  12913  cncongrprm  12918  oddpwdclemxy  12930  oddpwdclemodd  12933  qnumdenbi  12953  qnumgt0  12959  hashdvds  12982  crth  12985  fermltl  12995  modprminveq  13012  pcpremul  13055  pc2dvds  13092  pcz  13094  prmpwdvds  13117  4sqlem16  13168  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemodife  13223  ballotfilemrv1  13247  ballotfilemrv2  13248  ballotfilem1ri  13261  oddennn  13266  ctinfomlemom  13301  mgm1  13673  ismhm  13751  mhmpropd  13756  issubm  13762  issubm2  13763  grpsubrcan  13869  grplactcnv  13890  grp1  13894  eqgval  14009  eqgid  14012  quselbasg  14016  isghm  14029  conjnmzb  14066  iscmn  14079  eqgabl  14117  prdsbasmpt  14163  prdsbasmpt2  14171  rngmneg1  14229  rngmneg2  14230  rngpropd  14237  rngen1zr  14243  srgen1zr0  14275  ringideu  14304  ringpropd  14326  crngpropd  14327  dvdsrd  14384  dvdsr02  14395  opprunitd  14400  crngunit  14401  unitpropdg  14438  rhmunitinv  14468  isnzr2  14474  issubrng  14490  resrhm2b  14540  aprval  14574  aprunit  14575  isdrngtap  14589  opprdrng  14603  islmod  14610  islssm  14677  islssmg  14678  ellspsn  14737  isridl  14824  zrhrhmb  14940  zndvds  14967  znleval  14971  isassa  14985  istopg  15083  eltg  15136  eltg2  15137  tgss2  15163  bastop1  15167  bastop2  15168  iscld  15187  isnei  15228  neiint  15229  iscn  15281  iscnp  15283  iscnp3  15287  tgcn  15292  ssidcn  15294  lmbr2  15298  lmbrf  15299  cnnei  15316  cnrest2  15320  eltx  15343  imasnopn  15383  ispsmet  15407  ismet  15428  isxmet  15429  metn0  15462  xmetres2  15463  elbl3ps  15478  elbl3  15479  xblpnfps  15482  xblpnf  15483  elmopn2  15533  metss  15578  bdxmet  15585  metrest  15590  xmetxp  15591  xmetxpbl  15592  metcnp3  15595  metcnp  15596  metcnp2  15597  metcn  15598  txmetcnp  15602  txmetcn  15603  metcnpd  15604  bl2ioo  15634  addcncntoplem  15645  elcncf  15657  elcncf2  15658  ivthdec  15728  ellimc3apf  15744  cnlimcim  15755  dveflem  15810  ply1termlem  15826  sincosq2sgn  15911  sinq12gt0  15914  logltb  15958  ltexp2  16026  birthdaylem3  16072  wilthlem1  16077  lgsdilem  16129  lgsdir2lem4  16133  lgsdir2  16135  lgsne0  16140  lgsabs1  16141  gausslemma2dlem3  16165  gausslemma2dlem7  16170  lgseisenlem3  16174  lgsquad3  16186  2lgslem1a  16190  2lgslem3c  16197  2lgslem3d  16198  2lgsoddprmlem4  16214  2sqlem7  16223  2sqlem8a  16224  uhgreq12g  16300  isuhgropm  16305  uhgr0e  16306  upgrop  16328  uhgrvtxedgiedgb  16367  isuspgropen  16388  isusgropen  16389  uhgr2edg  16430  issubgr2  16482  uhgrspansubgrlem  16500  vtxd0nedgbfi  16523  1loopgrvd0fi  16530  iswlk  16547  upgriswlkdc  16584  istrl  16609  iseupth  16671  eupth2lem2dc  16683  eupth2lem3lem3fi  16694  eupth2lem3lem4fi  16697  eupth2lem3lem7fi  16698  cbvrald  16799  bj-nalset  16904  bj-sels  16923  bj-nnelirr  16962  isomninnlem  17053  iswomninnlem  17073  iswomni0  17075  ismkvnnlem  17076