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  800  con1biidc  884  pm4.54dc  909  dn1dc  968  dedlem0a  976  dfifp3dc  990  dfifp4dc  991  dfifp5dc  992  3bior2fd  1390  xorbi12d  1426  nbbndc  1438  eleq12d  2302  neeq12d  2422  neleq12d  2503  raleqbi1dv  2742  rexeqbi1dv  2743  reueqd  2744  rmoeqd  2745  raleqbidv  2746  rexeqbidv  2747  raleqbidva  2748  rexeqbidva  2749  eueq3dc  2980  sbc19.21g  3100  sbcabel  3114  sbcel1g  3146  sbceq1g  3147  sbcel2g  3148  sbceq2g  3149  sbccsb2g  3157  sbcco3g  3185  sseq12d  3258  raaanlem  3599  sbcssg  3603  ralsng  3709  2ralunsn  3882  csbunig  3901  disjeq12d  4073  breq123d  4102  sbcbr12g  4144  sbcbr1g  4145  sbcbr2g  4146  treq  4193  nalset  4219  exmidsssn  4292  copsex4g  4339  onsucb  4601  posng  4798  csbxpg  4807  sbcrel  4812  csbcnvg  4914  eliniseg  5106  brcodir  5124  csbrng  5198  sbcfung  5350  fneq12d  5422  feq12d  5472  feq123d  5473  sbcfng  5480  sbcfg  5481  f1osng  5626  csbfv12g  5679  funimass4  5696  dmfco  5714  eqfnfv  5744  eqfnfv2  5745  fneqeql2  5756  fvimacnvi  5761  funimass3  5763  fniniseg  5767  rexsupp  5771  unpreima  5772  ralrnmpt  5789  rexrnmpt  5790  dffo3  5794  fmptco  5813  fressnfv  5841  eufnfv  5885  foima2  5892  fnunirn  5908  dff13  5909  f1elima  5914  cocan1  5928  cocan2  5929  fliftel  5934  fliftf  5940  isoresbr  5950  isoini  5959  f1oiso  5967  f1ofveu  6006  mpoeq123dva  6082  ovid  6138  ov  6141  ovg  6161  ovelrn  6171  caovord2d  6192  ofrfval2  6252  offveqb  6255  eqop  6340  reldm  6349  f1od2  6400  mpoxopoveq  6406  mpoxopovel  6407  tpostpos  6430  smoiso  6468  frecabcl  6565  frecsuclem  6572  nnaordr  6678  nnaword  6679  nnaordex  6696  ereq1  6709  brdifun  6729  erth2  6749  qliftfun  6786  brecop  6794  elmapg  6830  elpmg  6833  dom2lem  6945  xpcomco  7010  pw2f1odclem  7020  php5fin  7071  elfi2  7171  supisolem  7207  inflbti  7223  inl11  7264  ismkvnex  7354  mkvprop  7357  nninfwlporlemd  7371  exmidfodomrlemreseldju  7411  ltapig  7558  ltmpig  7559  nlt1pig  7561  mulcmpblnq  7588  ltsonq  7618  lt2addnq  7624  lt2mulnq  7625  archnqq  7637  prarloclemarch  7638  ltrnqg  7640  mulcmpblnq0  7664  preqlu  7692  genpdflem  7727  addnqprllem  7747  addnqprulem  7748  addlocprlemgt  7754  appdivnq  7783  mulnqprl  7788  mulnqpru  7789  mullocprlem  7790  distrlem4prl  7804  distrlem4pru  7805  1idprl  7810  1idpru  7811  ltexprlemloc  7827  cauappcvgprlemladdrl  7877  cauappcvgprlemladd  7878  cauappcvgprlem1  7879  archrecnq  7883  caucvgprlemnkj  7886  caucvgprprlemexb  7927  addcmpblnr  7959  lttrsr  7982  ltsosr  7984  ltasrg  7990  mulextsr1  8001  srpospr  8003  caucvgsrlemcau  8013  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  map2psrprg  8025  ltresr  8059  axcaucvglemres  8119  eqlelt  8266  cnegexlem1  8354  negeu  8370  subadd2  8383  subcan2  8404  addrsub  8550  ltaddneg  8604  ltaddnegr  8605  ltadd1  8609  leadd2  8611  ltsubadd  8612  lesubadd  8614  ltaddsub2  8617  leaddsub2  8619  ltaddpos  8632  lesub2  8637  ltsub2  8639  ltnegcon1  8643  ltnegcon2  8644  lenegcon1  8646  lenegcon2  8647  addge01  8652  addge02  8653  suble0  8656  leaddle0  8657  lesub0  8659  eqord2  8664  sublt0d  8750  recexre  8758  reaplt  8768  reapltxor  8769  reapneg  8777  remulext1  8779  apreim  8783  apcotr  8787  apadd2  8789  addext  8790  apsub1  8822  mulcanap2d  8842  diveqap0  8862  diveqap1  8885  apmul2  8969  ltmul2  9036  lemul2  9037  ltmulgt11  9044  ltmulgt12  9045  gt0div  9050  ge0div  9051  ltmuldiv  9054  ltrec1  9068  lerec2  9069  ledivdiv  9070  ltdiv23  9072  lediv23  9073  suprleubex  9134  creur  9139  creui  9140  nn1suc  9162  nnrecl  9400  znnsub  9531  zgt0ge1  9538  zltlen  9558  nn0n0n1ge2b  9559  nn0le2is012  9562  btwnnz  9574  gtndiv  9575  prime  9579  eluz2  9761  indstr2  9843  negm  9849  nn01to3  9851  qapne  9873  qltlen  9874  qreccl  9876  irrmulap  9882  divlt1lt  9959  divle1le  9960  nnledivrp  10001  xnn0xadd0  10102  xltadd2  10112  xsubge0  10116  xlesubadd  10118  iccid  10160  elioc2  10171  elico2  10172  elicc2  10173  elfz2  10250  fzen  10278  fzsubel  10295  elfzp1  10307  fzpr  10312  fzrevral2  10341  fzrevral3  10342  nn0disj  10373  2ffzeq  10376  fzosplitsni  10482  fvinim0ffz  10488  ioo0  10520  ico0  10522  ioc0  10523  modq0  10592  negqmod0  10594  zmodidfzo  10616  frecuzrdgtcl  10675  nn0ennn  10696  nninfinf  10706  sq11  10875  nn0le2msqd  10982  nn0opth2d  10986  hashen  11047  zfz1isolem1  11105  zfz1iso  11106  csbwrdg  11144  wrdnval  11145  eqwrd  11155  ccat0  11174  ccatws1lenp1bg  11213  swrd0g  11242  swrdspsleq  11249  pfxeq  11278  pfxsuffeqwrdeq  11280  pfxsuff1eqwrdeq  11281  ccatopth2  11299  wrd2ind  11305  2shfti  11393  cjap  11468  cnreim  11540  rexfiuz  11551  rexanuz2  11553  abs00ap  11624  absext  11625  sqabs  11644  abslt  11650  absle  11651  absdiflt  11654  absdifle  11655  lenegsq  11657  minmax  11792  ltmininf  11797  mingeb  11804  xrminmax  11827  xrmin1inf  11829  xrmin2inf  11830  xrltmininf  11832  xrlemininf  11833  clim  11843  clim0c  11848  climrecvg1n  11910  zsumdc  11947  fsum2dlemstep  11997  binomlem  12046  pwm1geoserap1  12071  zproddc  12142  efieq  12298  sin01bnd  12320  cos01bnd  12321  dvdsval2  12353  modm1div  12363  zdvdsdc  12375  modmulconst  12386  dvdsaddr  12400  dvdsabseq  12410  fzocongeq  12421  zeo3  12431  odd2np1  12436  oddp1d2  12453  zob  12454  oddm1d2  12455  nnoddm1d2  12473  divalgb  12488  divalgmod  12490  modremain  12492  bits0  12511  bitsp1e  12515  bitsp1o  12516  bitscmp  12521  bitsinv1lem  12524  gcdn0gt0  12551  bezoutlemstep  12570  dvdssq  12604  nn0seqcvgd  12615  algcvgblem  12623  lcmdvds  12653  lcmgcdeq  12657  coprmdvds  12666  qredeq  12670  congr  12674  isprm2  12691  isprm3  12692  prmdvdsexp  12722  prmdvdsexpb  12723  prmexpb  12725  prmfac1  12726  cncongrprm  12731  oddpwdclemxy  12743  oddpwdclemodd  12746  qnumdenbi  12766  qnumgt0  12772  hashdvds  12795  crth  12798  fermltl  12808  modprminveq  12825  pcpremul  12868  pc2dvds  12905  pcz  12907  prmpwdvds  12930  4sqlem16  12981  oddennn  13015  ctinfomlemom  13050  prdsbasmpt  13365  prdsbasmpt2  13373  mgm1  13455  ismhm  13546  mhmpropd  13551  issubm  13557  issubm2  13558  grpsubrcan  13666  grplactcnv  13687  grp1  13691  eqgval  13812  eqgid  13815  quselbasg  13819  isghm  13832  conjnmzb  13869  iscmn  13882  eqgabl  13919  rngmneg1  13963  rngmneg2  13964  rngpropd  13971  srgen1zr  14004  ringideu  14033  ringpropd  14054  crngpropd  14055  dvdsrd  14111  dvdsr02  14122  opprunitd  14127  crngunit  14128  unitpropdg  14165  rhmunitinv  14195  isnzr2  14201  issubrng  14216  resrhm2b  14266  aprval  14299  islmod  14308  islssm  14374  islssmg  14375  ellspsn  14434  isridl  14521  zrhrhmb  14639  zndvds  14666  znleval  14670  istopg  14726  eltg  14779  eltg2  14780  tgss2  14806  bastop1  14810  bastop2  14811  iscld  14830  isnei  14871  neiint  14872  iscn  14924  iscnp  14926  iscnp3  14930  tgcn  14935  ssidcn  14937  lmbr2  14941  lmbrf  14942  cnnei  14959  cnrest2  14963  eltx  14986  imasnopn  15026  ispsmet  15050  ismet  15071  isxmet  15072  metn0  15105  xmetres2  15106  elbl3ps  15121  elbl3  15122  xblpnfps  15125  xblpnf  15126  elmopn2  15176  metss  15221  bdxmet  15228  metrest  15233  xmetxp  15234  xmetxpbl  15235  metcnp3  15238  metcnp  15239  metcnp2  15240  metcn  15241  txmetcnp  15245  txmetcn  15246  metcnpd  15247  bl2ioo  15277  addcncntoplem  15288  elcncf  15300  elcncf2  15301  ivthdec  15371  ellimc3apf  15387  cnlimcim  15398  dveflem  15453  ply1termlem  15469  sincosq2sgn  15554  sinq12gt0  15557  logltb  15601  ltexp2  15668  wilthlem1  15707  lgsdilem  15759  lgsdir2lem4  15763  lgsdir2  15765  lgsne0  15770  lgsabs1  15771  gausslemma2dlem3  15795  gausslemma2dlem7  15800  lgseisenlem3  15804  lgsquad3  15816  2lgslem1a  15820  2lgslem3c  15827  2lgslem3d  15828  2lgsoddprmlem4  15844  2sqlem7  15853  2sqlem8a  15854  uhgreq12g  15930  isuhgropm  15935  uhgr0e  15936  upgrop  15958  uhgrvtxedgiedgb  15997  isuspgropen  16018  isusgropen  16019  uhgr2edg  16060  issubgr2  16112  uhgrspansubgrlem  16130  vtxd0nedgbfi  16153  1loopgrvd0fi  16160  iswlk  16177  upgriswlkdc  16214  istrl  16239  iseupth  16301  eupth2lem2dc  16313  eupth2lem3lem3fi  16324  eupth2lem3lem4fi  16327  eupth2lem3lem7fi  16328  cbvrald  16405  bj-nalset  16511  bj-sels  16530  bj-nnelirr  16569  isomninnlem  16655  iswomninnlem  16674  iswomni0  16676  ismkvnnlem  16677