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 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3749  2ralunsn  3924  csbunig  3943  disjeq12d  4115  breq123d  4144  sbcbr12g  4186  sbcbr1g  4187  sbcbr2g  4188  treq  4235  nalset  4263  exmidsssn  4339  copsex4g  4387  onsucb  4650  posng  4847  csbxpg  4856  sbcrel  4861  csbcnvg  4964  eliniseg  5157  brcodir  5175  csbrng  5249  sbcfung  5401  fneq12d  5473  feq12d  5523  feq123d  5524  sbcfng  5531  sbcfg  5532  f1osng  5682  csbfv12g  5736  funimass4  5753  dmfco  5773  eqfnfv  5806  eqfnfv2  5807  fneqeql2  5818  fvimacnvi  5823  funimass3  5825  fniniseg  5829  unpreima  5833  ralrnmpt  5850  rexrnmpt  5851  dffo3  5855  fmptco  5874  fressnfv  5902  eufnfv  5949  foima2  5957  fnunirn  5973  dff13  5974  f1elima  5979  cocan1  5993  cocan2  5994  fliftel  5999  fliftf  6005  isoresbr  6015  isoini  6024  f1oiso  6032  f1ofveu  6073  mpoeq123dva  6149  ovid  6205  ov  6208  ovg  6228  ovelrn  6238  caovord2d  6259  ofrfval2  6319  offveqb  6322  eqop  6411  reldm  6420  f1od2  6471  suppval1  6479  suppssrst  6501  suppssrgst  6502  mpoxopoveq  6511  mpoxopovel  6512  tpostpos  6535  smoiso  6573  frecabcl  6670  frecsuclem  6677  nnaordr  6783  nnaword  6784  nnaordex  6801  ereq1  6814  brdifun  6834  erth2  6854  qliftfun  6891  brecop  6899  elmapg  6935  elpmg  6938  mapsnd  6970  dom2lem  7058  xpcomco  7124  pw2f1odclem  7134  php5fin  7186  funisfsupp  7291  ffsuppbi  7300  elfi2  7306  supisolem  7348  inflbti  7364  inl11  7405  ismkvnex  7495  mkvprop  7498  nninfwlporlemd  7512  exmidfodomrlemreseldju  7552  ltapig  7705  ltmpig  7706  nlt1pig  7708  mulcmpblnq  7735  ltsonq  7765  lt2addnq  7771  lt2mulnq  7772  archnqq  7784  prarloclemarch  7785  ltrnqg  7787  mulcmpblnq0  7811  preqlu  7839  genpdflem  7874  addnqprllem  7894  addnqprulem  7895  addlocprlemgt  7901  appdivnq  7930  mulnqprl  7935  mulnqpru  7936  mullocprlem  7937  distrlem4prl  7951  distrlem4pru  7952  1idprl  7957  1idpru  7958  ltexprlemloc  7974  cauappcvgprlemladdrl  8024  cauappcvgprlemladd  8025  cauappcvgprlem1  8026  archrecnq  8030  caucvgprlemnkj  8033  caucvgprprlemexb  8074  addcmpblnr  8106  lttrsr  8129  ltsosr  8131  ltasrg  8137  mulextsr1  8148  srpospr  8150  caucvgsrlemcau  8160  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  map2psrprg  8172  ltresr  8206  axcaucvglemres  8266  eqlelt  8412  cnegexlem1  8501  negeu  8517  subadd2  8530  subcan2  8551  addrsub  8697  ltaddneg  8752  ltaddnegr  8753  ltadd1  8757  leadd2  8759  ltsubadd  8760  lesubadd  8762  ltaddsub2  8765  leaddsub2  8767  ltaddpos  8780  lesub2  8785  ltsub2  8787  ltnegcon1  8791  ltnegcon2  8792  lenegcon1  8794  lenegcon2  8795  addge01  8800  addge02  8801  suble0  8804  leaddle0  8805  lesub0  8807  eqord2  8812  sublt0d  8899  recexre  8907  reaplt  8917  reapltxor  8918  reapneg  8926  remulext1  8928  apreim  8932  apcotr  8936  apadd2  8938  addext  8939  apsub1  8971  mulcanap2d  8991  diveqap0  9013  diveqap1  9036  apmul2  9120  ltmul2  9187  lemul2  9188  ltmulgt11  9195  ltmulgt12  9196  gt0div  9201  ge0div  9202  ltmuldiv  9205  ltrec1  9219  lerec2  9220  ledivdiv  9221  ltdiv23  9223  lediv23  9224  suprleubex  9285  creur  9290  creui  9291  nn1suc  9324  nnrecl  9563  fcdmnn0fsuppg  9620  znnsub  9698  zgt0ge1  9705  zltlen  9726  nn0n0n1ge2b  9727  nn0le2is012  9730  btwnnz  9742  gtndiv  9743  prime  9747  eluz2  9929  indstr2  10011  negm  10017  nn01to3  10019  qapne  10041  qltlen  10042  qreccl  10044  irrmulap  10050  divlt1lt  10127  divle1le  10128  nnledivrp  10169  xnn0xadd0  10271  xltadd2  10281  xsubge0  10285  xlesubadd  10287  iccid  10329  elioc2  10340  elico2  10341  elicc2  10342  elfz2  10420  fzen  10449  fzsubel  10468  elfzp1  10481  fzpr  10486  fzrevral2  10515  fzrevral3  10516  nn0disj  10547  2ffzeq  10550  fzosplitsni  10656  fvinim0ffz  10662  ioo0  10696  ico0  10698  ioc0  10699  modq0  10768  negqmod0  10770  zmodidfzo  10792  frecuzrdgtcl  10851  nn0ennn  10872  nninfinf  10882  sq11  11051  nn0le2msqd  11159  nn0opth2d  11163  hashen  11225  zfz1isolem1  11294  zfz1iso  11295  csbwrdg  11336  wrdnval  11337  eqwrd  11347  ccat0  11366  ccatws1lenp1bg  11405  swrd0g  11434  swrdspsleq  11441  pfxeq  11470  pfxsuffeqwrdeq  11472  pfxsuff1eqwrdeq  11473  ccatopth2  11491  wrd2ind  11497  2shfti  11598  cjap  11674  cnreim  11746  rexfiuz  11757  rexanuz2  11759  abs00ap  11830  absext  11831  sqabs  11850  abslt  11856  absle  11857  absdiflt  11860  absdifle  11861  lenegsq  11863  minmax  11998  ltmininf  12003  mingeb  12010  xrminmax  12033  xrmin1inf  12035  xrmin2inf  12036  xrltmininf  12038  xrlemininf  12039  clim  12049  clim0c  12054  climrecvg1n  12116  zsumdc  12153  fsum2dlemstep  12203  binomlem  12252  pwm1geoserap1  12277  zproddc  12348  efieq  12504  sin01bnd  12526  cos01bnd  12527  dvdsval2  12559  modm1div  12569  zdvdsdc  12581  modmulconst  12592  dvdsaddr  12606  dvdsabseq  12616  fzocongeq  12627  zeo3  12637  odd2np1  12642  oddp1d2  12659  zob  12660  oddm1d2  12661  nnoddm1d2  12679  divalgb  12694  divalgmod  12696  modremain  12698  bits0  12717  bitsp1e  12721  bitsp1o  12722  bitscmp  12727  bitsinv1lem  12730  gcdn0gt0  12757  bezoutlemstep  12776  dvdssq  12810  nn0seqcvgd  12821  algcvgblem  12829  lcmdvds  12859  lcmgcdeq  12863  coprmdvds  12872  qredeq  12876  congr  12880  isprm2  12897  isprm3  12898  prmdvdsexp  12928  prmdvdsexpb  12929  prmexpb  12931  prmfac1  12932  cncongrprm  12937  oddpwdclemxy  12949  oddpwdclemodd  12952  qnumdenbi  12972  qnumgt0  12978  hashdvds  13001  crth  13004  fermltl  13014  modprminveq  13031  pcpremul  13074  pc2dvds  13111  pcz  13113  prmpwdvds  13136  4sqlem16  13187  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemodife  13242  ballotfilemrv1  13266  ballotfilemrv2  13267  ballotfilem1ri  13280  oddennn  13285  ctinfomlemom  13320  mgm1  13692  ismhm  13770  mhmpropd  13775  issubm  13781  issubm2  13782  grpsubrcan  13888  grplactcnv  13909  grp1  13913  eqgval  14028  eqgid  14031  quselbasg  14035  isghm  14048  conjnmzb  14085  iscmn  14098  eqgabl  14136  prdsbasmpt  14182  prdsbasmpt2  14190  rngmneg1  14248  rngmneg2  14249  rngpropd  14256  rngen1zr  14262  srgen1zr0  14294  ringideu  14323  ringpropd  14345  crngpropd  14346  dvdsrd  14403  dvdsr02  14414  opprunitd  14419  crngunit  14420  unitpropdg  14457  rhmunitinv  14487  isnzr2  14493  issubrng  14509  resrhm2b  14559  aprval  14593  aprunit  14594  isdrngtap  14608  opprdrng  14622  islmod  14629  islssm  14696  islssmg  14697  ellspsn  14756  isridl  14843  zrhrhmb  14959  zndvds  14986  znleval  14990  isassa  15004  istopg  15102  eltg  15155  eltg2  15156  tgss2  15182  bastop1  15186  bastop2  15187  iscld  15206  isnei  15247  neiint  15248  iscn  15300  iscnp  15302  iscnp3  15306  tgcn  15311  ssidcn  15313  lmbr2  15317  lmbrf  15318  cnnei  15335  cnrest2  15339  eltx  15362  imasnopn  15402  ispsmet  15426  ismet  15447  isxmet  15448  metn0  15481  xmetres2  15482  elbl3ps  15497  elbl3  15498  xblpnfps  15501  xblpnf  15502  elmopn2  15552  metss  15597  bdxmet  15604  metrest  15609  xmetxp  15610  xmetxpbl  15611  metcnp3  15614  metcnp  15615  metcnp2  15616  metcn  15617  txmetcnp  15621  txmetcn  15622  metcnpd  15623  bl2ioo  15653  addcncntoplem  15664  elcncf  15676  elcncf2  15677  ivthdec  15747  ellimc3apf  15763  cnlimcim  15774  dveflem  15829  ply1termlem  15845  sincosq2sgn  15931  sinq12gt0  15934  logltb  15979  ltexp2  16049  birthdaylem3  16095  wilthlem1  16100  lgsdilem  16158  lgsdir2lem4  16162  lgsdir2  16164  lgsne0  16169  lgsabs1  16170  gausslemma2dlem3  16194  gausslemma2dlem7  16199  lgseisenlem3  16203  lgsquad3  16215  2lgslem1a  16219  2lgslem3c  16226  2lgslem3d  16227  2lgsoddprmlem4  16243  2sqlem7  16252  2sqlem8a  16253  uhgreq12g  16329  isuhgropm  16334  uhgr0e  16335  upgrop  16357  uhgrvtxedgiedgb  16396  isuspgropen  16417  isusgropen  16418  uhgr2edg  16459  issubgr2  16511  uhgrspansubgrlem  16529  vtxd0nedgbfi  16552  1loopgrvd0fi  16559  iswlk  16576  upgriswlkdc  16613  istrl  16638  iseupth  16700  eupth2lem2dc  16712  eupth2lem3lem3fi  16723  eupth2lem3lem4fi  16726  eupth2lem3lem7fi  16727  cbvrald  16828  bj-nalset  16933  bj-sels  16952  bj-nnelirr  16991  stnot  17051  isomninnlem  17091  iswomninnlem  17111  iswomni0  17113  ismkvnnlem  17114