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  798  con1biidc  882  pm4.54dc  907  dn1dc  966  dedlem0a  974  dfifp3dc  988  dfifp4dc  989  dfifp5dc  990  3bior2fd  1388  xorbi12d  1424  nbbndc  1436  eleq12d  2300  neeq12d  2420  neleq12d  2501  raleqbi1dv  2740  rexeqbi1dv  2741  reueqd  2742  rmoeqd  2743  raleqbidv  2744  rexeqbidv  2745  raleqbidva  2746  rexeqbidva  2747  eueq3dc  2977  sbc19.21g  3097  sbcabel  3111  sbcel1g  3143  sbceq1g  3144  sbcel2g  3145  sbceq2g  3146  sbccsb2g  3154  sbcco3g  3182  sseq12d  3255  raaanlem  3596  sbcssg  3600  ralsng  3706  2ralunsn  3877  csbunig  3896  disjeq12d  4068  breq123d  4097  sbcbr12g  4139  sbcbr1g  4140  sbcbr2g  4141  treq  4188  nalset  4214  exmidsssn  4287  copsex4g  4334  onsucb  4596  posng  4793  csbxpg  4802  sbcrel  4807  csbcnvg  4909  eliniseg  5101  brcodir  5119  csbrng  5193  sbcfung  5345  fneq12d  5416  feq12d  5466  feq123d  5467  sbcfng  5474  sbcfg  5475  f1osng  5619  csbfv12g  5672  funimass4  5689  dmfco  5707  eqfnfv  5737  eqfnfv2  5738  fneqeql2  5749  fvimacnvi  5754  funimass3  5756  fniniseg  5760  rexsupp  5764  unpreima  5765  ralrnmpt  5782  rexrnmpt  5783  dffo3  5787  fmptco  5806  fressnfv  5833  eufnfv  5877  foima2  5884  fnunirn  5900  dff13  5901  f1elima  5906  cocan1  5920  cocan2  5921  fliftel  5926  fliftf  5932  isoresbr  5942  isoini  5951  f1oiso  5959  f1ofveu  5998  mpoeq123dva  6074  ovid  6130  ov  6133  ovg  6153  ovelrn  6163  caovord2d  6184  ofrfval2  6244  offveqb  6247  eqop  6332  reldm  6341  f1od2  6392  mpoxopoveq  6397  mpoxopovel  6398  tpostpos  6421  smoiso  6459  frecabcl  6556  frecsuclem  6563  nnaordr  6669  nnaword  6670  nnaordex  6687  ereq1  6700  brdifun  6720  erth2  6740  qliftfun  6777  brecop  6785  elmapg  6821  elpmg  6824  dom2lem  6936  xpcomco  6998  pw2f1odclem  7008  php5fin  7057  elfi2  7155  supisolem  7191  inflbti  7207  inl11  7248  ismkvnex  7338  mkvprop  7341  nninfwlporlemd  7355  exmidfodomrlemreseldju  7394  ltapig  7541  ltmpig  7542  nlt1pig  7544  mulcmpblnq  7571  ltsonq  7601  lt2addnq  7607  lt2mulnq  7608  archnqq  7620  prarloclemarch  7621  ltrnqg  7623  mulcmpblnq0  7647  preqlu  7675  genpdflem  7710  addnqprllem  7730  addnqprulem  7731  addlocprlemgt  7737  appdivnq  7766  mulnqprl  7771  mulnqpru  7772  mullocprlem  7773  distrlem4prl  7787  distrlem4pru  7788  1idprl  7793  1idpru  7794  ltexprlemloc  7810  cauappcvgprlemladdrl  7860  cauappcvgprlemladd  7861  cauappcvgprlem1  7862  archrecnq  7866  caucvgprlemnkj  7869  caucvgprprlemexb  7910  addcmpblnr  7942  lttrsr  7965  ltsosr  7967  ltasrg  7973  mulextsr1  7984  srpospr  7986  caucvgsrlemcau  7996  caucvgsrlemgt1  7998  caucvgsrlemoffres  8003  map2psrprg  8008  ltresr  8042  axcaucvglemres  8102  eqlelt  8249  cnegexlem1  8337  negeu  8353  subadd2  8366  subcan2  8387  addrsub  8533  ltaddneg  8587  ltaddnegr  8588  ltadd1  8592  leadd2  8594  ltsubadd  8595  lesubadd  8597  ltaddsub2  8600  leaddsub2  8602  ltaddpos  8615  lesub2  8620  ltsub2  8622  ltnegcon1  8626  ltnegcon2  8627  lenegcon1  8629  lenegcon2  8630  addge01  8635  addge02  8636  suble0  8639  leaddle0  8640  lesub0  8642  eqord2  8647  sublt0d  8733  recexre  8741  reaplt  8751  reapltxor  8752  reapneg  8760  remulext1  8762  apreim  8766  apcotr  8770  apadd2  8772  addext  8773  apsub1  8805  mulcanap2d  8825  diveqap0  8845  diveqap1  8868  apmul2  8952  ltmul2  9019  lemul2  9020  ltmulgt11  9027  ltmulgt12  9028  gt0div  9033  ge0div  9034  ltmuldiv  9037  ltrec1  9051  lerec2  9052  ledivdiv  9053  ltdiv23  9055  lediv23  9056  suprleubex  9117  creur  9122  creui  9123  nn1suc  9145  nnrecl  9383  znnsub  9514  zgt0ge1  9521  zltlen  9541  nn0n0n1ge2b  9542  nn0le2is012  9545  btwnnz  9557  gtndiv  9558  prime  9562  eluz2  9744  indstr2  9821  negm  9827  nn01to3  9829  qapne  9851  qltlen  9852  qreccl  9854  irrmulap  9860  divlt1lt  9937  divle1le  9938  nnledivrp  9979  xnn0xadd0  10080  xltadd2  10090  xsubge0  10094  xlesubadd  10096  iccid  10138  elioc2  10149  elico2  10150  elicc2  10151  elfz2  10228  fzen  10256  fzsubel  10273  elfzp1  10285  fzpr  10290  fzrevral2  10319  fzrevral3  10320  nn0disj  10351  2ffzeq  10354  fzosplitsni  10458  fvinim0ffz  10464  ioo0  10496  ico0  10498  ioc0  10499  modq0  10568  negqmod0  10570  zmodidfzo  10592  frecuzrdgtcl  10651  nn0ennn  10672  nninfinf  10682  sq11  10851  nn0le2msqd  10958  nn0opth2d  10962  hashen  11023  zfz1isolem1  11080  zfz1iso  11081  csbwrdg  11119  wrdnval  11120  eqwrd  11130  ccat0  11149  ccatws1lenp1bg  11188  swrd0g  11213  swrdspsleq  11220  pfxeq  11249  pfxsuffeqwrdeq  11251  pfxsuff1eqwrdeq  11252  ccatopth2  11270  wrd2ind  11276  2shfti  11363  cjap  11438  cnreim  11510  rexfiuz  11521  rexanuz2  11523  abs00ap  11594  absext  11595  sqabs  11614  abslt  11620  absle  11621  absdiflt  11624  absdifle  11625  lenegsq  11627  minmax  11762  ltmininf  11767  mingeb  11774  xrminmax  11797  xrmin1inf  11799  xrmin2inf  11800  xrltmininf  11802  xrlemininf  11803  clim  11813  clim0c  11818  climrecvg1n  11880  zsumdc  11916  fsum2dlemstep  11966  binomlem  12015  pwm1geoserap1  12040  zproddc  12111  efieq  12267  sin01bnd  12289  cos01bnd  12290  dvdsval2  12322  modm1div  12332  zdvdsdc  12344  modmulconst  12355  dvdsaddr  12369  dvdsabseq  12379  fzocongeq  12390  zeo3  12400  odd2np1  12405  oddp1d2  12422  zob  12423  oddm1d2  12424  nnoddm1d2  12442  divalgb  12457  divalgmod  12459  modremain  12461  bits0  12480  bitsp1e  12484  bitsp1o  12485  bitscmp  12490  bitsinv1lem  12493  gcdn0gt0  12520  bezoutlemstep  12539  dvdssq  12573  nn0seqcvgd  12584  algcvgblem  12592  lcmdvds  12622  lcmgcdeq  12626  coprmdvds  12635  qredeq  12639  congr  12643  isprm2  12660  isprm3  12661  prmdvdsexp  12691  prmdvdsexpb  12692  prmexpb  12694  prmfac1  12695  cncongrprm  12700  oddpwdclemxy  12712  oddpwdclemodd  12715  qnumdenbi  12735  qnumgt0  12741  hashdvds  12764  crth  12767  fermltl  12777  modprminveq  12794  pcpremul  12837  pc2dvds  12874  pcz  12876  prmpwdvds  12899  4sqlem16  12950  oddennn  12984  ctinfomlemom  13019  prdsbasmpt  13334  prdsbasmpt2  13342  mgm1  13424  ismhm  13515  mhmpropd  13520  issubm  13526  issubm2  13527  grpsubrcan  13635  grplactcnv  13656  grp1  13660  eqgval  13781  eqgid  13784  quselbasg  13788  isghm  13801  conjnmzb  13838  iscmn  13851  eqgabl  13888  rngmneg1  13931  rngmneg2  13932  rngpropd  13939  srgen1zr  13972  ringideu  14001  ringpropd  14022  crngpropd  14023  dvdsrd  14079  dvdsr02  14090  opprunitd  14095  crngunit  14096  unitpropdg  14133  rhmunitinv  14163  isnzr2  14169  issubrng  14184  resrhm2b  14234  aprval  14267  islmod  14276  islssm  14342  islssmg  14343  ellspsn  14402  isridl  14489  zrhrhmb  14607  zndvds  14634  znleval  14638  istopg  14694  eltg  14747  eltg2  14748  tgss2  14774  bastop1  14778  bastop2  14779  iscld  14798  isnei  14839  neiint  14840  iscn  14892  iscnp  14894  iscnp3  14898  tgcn  14903  ssidcn  14905  lmbr2  14909  lmbrf  14910  cnnei  14927  cnrest2  14931  eltx  14954  imasnopn  14994  ispsmet  15018  ismet  15039  isxmet  15040  metn0  15073  xmetres2  15074  elbl3ps  15089  elbl3  15090  xblpnfps  15093  xblpnf  15094  elmopn2  15144  metss  15189  bdxmet  15196  metrest  15201  xmetxp  15202  xmetxpbl  15203  metcnp3  15206  metcnp  15207  metcnp2  15208  metcn  15209  txmetcnp  15213  txmetcn  15214  metcnpd  15215  bl2ioo  15245  addcncntoplem  15256  elcncf  15268  elcncf2  15269  ivthdec  15339  ellimc3apf  15355  cnlimcim  15366  dveflem  15421  ply1termlem  15437  sincosq2sgn  15522  sinq12gt0  15525  logltb  15569  ltexp2  15636  wilthlem1  15675  lgsdilem  15727  lgsdir2lem4  15731  lgsdir2  15733  lgsne0  15738  lgsabs1  15739  gausslemma2dlem3  15763  gausslemma2dlem7  15768  lgseisenlem3  15772  lgsquad3  15784  2lgslem1a  15788  2lgslem3c  15795  2lgslem3d  15796  2lgsoddprmlem4  15812  2sqlem7  15821  2sqlem8a  15822  uhgreq12g  15897  isuhgropm  15902  uhgr0e  15903  upgrop  15925  uhgrvtxedgiedgb  15962  isuspgropen  15983  isusgropen  15984  uhgr2edg  16025  vtxd0nedgbfi  16085  iswlk  16095  upgriswlkdc  16132  istrl  16155  cbvrald  16261  bj-nalset  16367  bj-sels  16386  bj-nnelirr  16425  isomninnlem  16512  iswomninnlem  16531  iswomni0  16533  ismkvnnlem  16534