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  794  con1biidc  878  pm4.54dc  903  dn1dc  962  dedlem0a  970  xorbi12d  1393  nbbndc  1405  eleq12d  2264  neeq12d  2384  neleq12d  2465  raleqbi1dv  2702  rexeqbi1dv  2703  reueqd  2704  rmoeqd  2705  raleqbidv  2706  rexeqbidv  2707  raleqbidva  2708  rexeqbidva  2709  eueq3dc  2934  sbc19.21g  3054  sbcabel  3067  sbcel1g  3099  sbceq1g  3100  sbcel2g  3101  sbceq2g  3102  sbccsb2g  3110  sbcco3g  3138  sseq12d  3210  raaanlem  3551  sbcssg  3555  ralsng  3658  2ralunsn  3824  csbunig  3843  disjeq12d  4015  breq123d  4043  sbcbr12g  4084  sbcbr1g  4085  sbcbr2g  4086  treq  4133  nalset  4159  exmidsssn  4231  copsex4g  4276  onsucb  4535  posng  4731  csbxpg  4740  sbcrel  4745  csbcnvg  4846  eliniseg  5035  brcodir  5053  csbrng  5127  sbcfung  5278  fneq12d  5346  feq12d  5393  feq123d  5394  sbcfng  5401  sbcfg  5402  f1osng  5541  csbfv12g  5592  funimass4  5607  dmfco  5625  eqfnfv  5655  eqfnfv2  5656  fneqeql2  5667  fvimacnvi  5672  funimass3  5674  fniniseg  5678  rexsupp  5682  unpreima  5683  ralrnmpt  5700  rexrnmpt  5701  dffo3  5705  fmptco  5724  fressnfv  5745  eufnfv  5789  foima2  5794  fnunirn  5810  dff13  5811  f1elima  5816  cocan1  5830  cocan2  5831  fliftel  5836  fliftf  5842  isoresbr  5852  isoini  5861  f1oiso  5869  f1ofveu  5906  mpoeq123dva  5979  ovid  6035  ov  6038  ovg  6057  ovelrn  6067  caovord2d  6088  ofrfval2  6147  offveqb  6150  eqop  6230  reldm  6239  f1od2  6288  mpoxopoveq  6293  mpoxopovel  6294  tpostpos  6317  smoiso  6355  frecabcl  6452  frecsuclem  6459  nnaordr  6563  nnaword  6564  nnaordex  6581  ereq1  6594  brdifun  6614  erth2  6634  qliftfun  6671  brecop  6679  elmapg  6715  elpmg  6718  dom2lem  6826  xpcomco  6880  pw2f1odclem  6890  php5fin  6938  elfi2  7031  supisolem  7067  inflbti  7083  inl11  7124  ismkvnex  7214  mkvprop  7217  nninfwlporlemd  7231  exmidfodomrlemreseldju  7260  ltapig  7398  ltmpig  7399  nlt1pig  7401  mulcmpblnq  7428  ltsonq  7458  lt2addnq  7464  lt2mulnq  7465  archnqq  7477  prarloclemarch  7478  ltrnqg  7480  mulcmpblnq0  7504  preqlu  7532  genpdflem  7567  addnqprllem  7587  addnqprulem  7588  addlocprlemgt  7594  appdivnq  7623  mulnqprl  7628  mulnqpru  7629  mullocprlem  7630  distrlem4prl  7644  distrlem4pru  7645  1idprl  7650  1idpru  7651  ltexprlemloc  7667  cauappcvgprlemladdrl  7717  cauappcvgprlemladd  7718  cauappcvgprlem1  7719  archrecnq  7723  caucvgprlemnkj  7726  caucvgprprlemexb  7767  addcmpblnr  7799  lttrsr  7822  ltsosr  7824  ltasrg  7830  mulextsr1  7841  srpospr  7843  caucvgsrlemcau  7853  caucvgsrlemgt1  7855  caucvgsrlemoffres  7860  map2psrprg  7865  ltresr  7899  axcaucvglemres  7959  eqlelt  8106  cnegexlem1  8194  negeu  8210  subadd2  8223  subcan2  8244  addrsub  8390  ltaddneg  8443  ltaddnegr  8444  ltadd1  8448  leadd2  8450  ltsubadd  8451  lesubadd  8453  ltaddsub2  8456  leaddsub2  8458  ltaddpos  8471  lesub2  8476  ltsub2  8478  ltnegcon1  8482  ltnegcon2  8483  lenegcon1  8485  lenegcon2  8486  addge01  8491  addge02  8492  suble0  8495  leaddle0  8496  lesub0  8498  eqord2  8503  sublt0d  8589  recexre  8597  reaplt  8607  reapltxor  8608  reapneg  8616  remulext1  8618  apreim  8622  apcotr  8626  apadd2  8628  addext  8629  apsub1  8661  mulcanap2d  8681  diveqap0  8701  diveqap1  8724  apmul2  8808  ltmul2  8875  lemul2  8876  ltmulgt11  8883  ltmulgt12  8884  gt0div  8889  ge0div  8890  ltmuldiv  8893  ltrec1  8907  lerec2  8908  ledivdiv  8909  ltdiv23  8911  lediv23  8912  suprleubex  8973  creur  8978  creui  8979  nn1suc  9001  nnrecl  9238  znnsub  9368  zgt0ge1  9375  zltlen  9395  nn0n0n1ge2b  9396  nn0le2is012  9399  btwnnz  9411  gtndiv  9412  prime  9416  eluz2  9598  indstr2  9674  negm  9680  nn01to3  9682  qapne  9704  qltlen  9705  qreccl  9707  irrmulap  9713  divlt1lt  9790  divle1le  9791  nnledivrp  9832  xnn0xadd0  9933  xltadd2  9943  xsubge0  9947  xlesubadd  9949  iccid  9991  elioc2  10002  elico2  10003  elicc2  10004  elfz2  10081  fzen  10109  fzsubel  10126  elfzp1  10138  fzpr  10143  fzrevral2  10172  fzrevral3  10173  nn0disj  10204  2ffzeq  10207  fzosplitsni  10302  fvinim0ffz  10308  ioo0  10328  ico0  10330  ioc0  10331  modq0  10400  negqmod0  10402  zmodidfzo  10424  frecuzrdgtcl  10483  nn0ennn  10504  nninfinf  10514  sq11  10683  nn0le2msqd  10790  nn0opth2d  10794  hashen  10855  zfz1isolem1  10911  zfz1iso  10912  csbwrdg  10943  wrdnval  10944  eqwrd  10954  2shfti  10975  cjap  11050  cnreim  11122  rexfiuz  11133  rexanuz2  11135  abs00ap  11206  absext  11207  sqabs  11226  abslt  11232  absle  11233  absdiflt  11236  absdifle  11237  lenegsq  11239  minmax  11373  ltmininf  11378  mingeb  11385  xrminmax  11408  xrmin1inf  11410  xrmin2inf  11411  xrltmininf  11413  xrlemininf  11414  clim  11424  clim0c  11429  climrecvg1n  11491  zsumdc  11527  fsum2dlemstep  11577  binomlem  11626  pwm1geoserap1  11651  zproddc  11722  efieq  11878  sin01bnd  11900  cos01bnd  11901  dvdsval2  11933  modm1div  11943  zdvdsdc  11955  modmulconst  11966  dvdsaddr  11980  dvdsabseq  11989  fzocongeq  12000  zeo3  12009  odd2np1  12014  oddp1d2  12031  zob  12032  oddm1d2  12033  nnoddm1d2  12051  divalgb  12066  divalgmod  12068  modremain  12070  gcdn0gt0  12115  bezoutlemstep  12134  dvdssq  12168  nn0seqcvgd  12179  algcvgblem  12187  lcmdvds  12217  lcmgcdeq  12221  coprmdvds  12230  qredeq  12234  congr  12238  isprm2  12255  isprm3  12256  prmdvdsexp  12286  prmdvdsexpb  12287  prmexpb  12289  prmfac1  12290  cncongrprm  12295  oddpwdclemxy  12307  oddpwdclemodd  12310  qnumdenbi  12330  qnumgt0  12336  hashdvds  12359  crth  12362  fermltl  12372  modprminveq  12388  pcpremul  12431  pc2dvds  12468  pcz  12470  prmpwdvds  12493  4sqlem16  12544  oddennn  12549  ctinfomlemom  12584  mgm1  12953  ismhm  13033  mhmpropd  13038  issubm  13044  issubm2  13045  grpsubrcan  13153  grplactcnv  13174  grp1  13178  eqgval  13293  eqgid  13296  quselbasg  13300  isghm  13313  conjnmzb  13350  iscmn  13363  eqgabl  13400  rngmneg1  13443  rngmneg2  13444  rngpropd  13451  srgen1zr  13484  ringideu  13513  ringpropd  13534  crngpropd  13535  dvdsrd  13590  dvdsr02  13601  opprunitd  13606  crngunit  13607  unitpropdg  13644  rhmunitinv  13674  isnzr2  13680  issubrng  13695  resrhm2b  13745  aprval  13778  islmod  13787  islssm  13853  islssmg  13854  ellspsn  13913  isridl  14000  zrhrhmb  14110  zndvds  14137  znleval  14141  istopg  14167  eltg  14220  eltg2  14221  tgss2  14247  bastop1  14251  bastop2  14252  iscld  14271  isnei  14312  neiint  14313  iscn  14365  iscnp  14367  iscnp3  14371  tgcn  14376  ssidcn  14378  lmbr2  14382  lmbrf  14383  cnnei  14400  cnrest2  14404  eltx  14427  imasnopn  14467  ispsmet  14491  ismet  14512  isxmet  14513  metn0  14546  xmetres2  14547  elbl3ps  14562  elbl3  14563  xblpnfps  14566  xblpnf  14567  elmopn2  14617  metss  14662  bdxmet  14669  metrest  14674  xmetxp  14675  xmetxpbl  14676  metcnp3  14679  metcnp  14680  metcnp2  14681  metcn  14682  txmetcnp  14686  txmetcn  14687  metcnpd  14688  bl2ioo  14710  addcncntoplem  14719  elcncf  14728  elcncf2  14729  ivthdec  14798  ellimc3apf  14814  cnlimcim  14825  dveflem  14872  ply1termlem  14888  sincosq2sgn  14962  sinq12gt0  14965  logltb  15009  ltexp2  15074  wilthlem1  15112  lgsdilem  15143  lgsdir2lem4  15147  lgsdir2  15149  lgsne0  15154  lgsabs1  15155  gausslemma2dlem3  15179  gausslemma2dlem7  15184  lgseisenlem3  15188  2lgsoddprmlem4  15200  2sqlem7  15208  2sqlem8a  15209  cbvrald  15280  bj-nalset  15387  bj-sels  15406  bj-nnelirr  15445  isomninnlem  15520  iswomninnlem  15539  iswomni0  15541  ismkvnnlem  15542