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  2978  sbc19.21g  3098  sbcabel  3112  sbcel1g  3144  sbceq1g  3145  sbcel2g  3146  sbceq2g  3147  sbccsb2g  3155  sbcco3g  3183  sseq12d  3256  raaanlem  3597  sbcssg  3601  ralsng  3707  2ralunsn  3880  csbunig  3899  disjeq12d  4071  breq123d  4100  sbcbr12g  4142  sbcbr1g  4143  sbcbr2g  4144  treq  4191  nalset  4217  exmidsssn  4290  copsex4g  4337  onsucb  4599  posng  4796  csbxpg  4805  sbcrel  4810  csbcnvg  4912  eliniseg  5104  brcodir  5122  csbrng  5196  sbcfung  5348  fneq12d  5419  feq12d  5469  feq123d  5470  sbcfng  5477  sbcfg  5478  f1osng  5622  csbfv12g  5675  funimass4  5692  dmfco  5710  eqfnfv  5740  eqfnfv2  5741  fneqeql2  5752  fvimacnvi  5757  funimass3  5759  fniniseg  5763  rexsupp  5767  unpreima  5768  ralrnmpt  5785  rexrnmpt  5786  dffo3  5790  fmptco  5809  fressnfv  5836  eufnfv  5880  foima2  5887  fnunirn  5903  dff13  5904  f1elima  5909  cocan1  5923  cocan2  5924  fliftel  5929  fliftf  5935  isoresbr  5945  isoini  5954  f1oiso  5962  f1ofveu  6001  mpoeq123dva  6077  ovid  6133  ov  6136  ovg  6156  ovelrn  6166  caovord2d  6187  ofrfval2  6247  offveqb  6250  eqop  6335  reldm  6344  f1od2  6395  mpoxopoveq  6401  mpoxopovel  6402  tpostpos  6425  smoiso  6463  frecabcl  6560  frecsuclem  6567  nnaordr  6673  nnaword  6674  nnaordex  6691  ereq1  6704  brdifun  6724  erth2  6744  qliftfun  6781  brecop  6789  elmapg  6825  elpmg  6828  dom2lem  6940  xpcomco  7005  pw2f1odclem  7015  php5fin  7066  elfi2  7165  supisolem  7201  inflbti  7217  inl11  7258  ismkvnex  7348  mkvprop  7351  nninfwlporlemd  7365  exmidfodomrlemreseldju  7404  ltapig  7551  ltmpig  7552  nlt1pig  7554  mulcmpblnq  7581  ltsonq  7611  lt2addnq  7617  lt2mulnq  7618  archnqq  7630  prarloclemarch  7631  ltrnqg  7633  mulcmpblnq0  7657  preqlu  7685  genpdflem  7720  addnqprllem  7740  addnqprulem  7741  addlocprlemgt  7747  appdivnq  7776  mulnqprl  7781  mulnqpru  7782  mullocprlem  7783  distrlem4prl  7797  distrlem4pru  7798  1idprl  7803  1idpru  7804  ltexprlemloc  7820  cauappcvgprlemladdrl  7870  cauappcvgprlemladd  7871  cauappcvgprlem1  7872  archrecnq  7876  caucvgprlemnkj  7879  caucvgprprlemexb  7920  addcmpblnr  7952  lttrsr  7975  ltsosr  7977  ltasrg  7983  mulextsr1  7994  srpospr  7996  caucvgsrlemcau  8006  caucvgsrlemgt1  8008  caucvgsrlemoffres  8013  map2psrprg  8018  ltresr  8052  axcaucvglemres  8112  eqlelt  8259  cnegexlem1  8347  negeu  8363  subadd2  8376  subcan2  8397  addrsub  8543  ltaddneg  8597  ltaddnegr  8598  ltadd1  8602  leadd2  8604  ltsubadd  8605  lesubadd  8607  ltaddsub2  8610  leaddsub2  8612  ltaddpos  8625  lesub2  8630  ltsub2  8632  ltnegcon1  8636  ltnegcon2  8637  lenegcon1  8639  lenegcon2  8640  addge01  8645  addge02  8646  suble0  8649  leaddle0  8650  lesub0  8652  eqord2  8657  sublt0d  8743  recexre  8751  reaplt  8761  reapltxor  8762  reapneg  8770  remulext1  8772  apreim  8776  apcotr  8780  apadd2  8782  addext  8783  apsub1  8815  mulcanap2d  8835  diveqap0  8855  diveqap1  8878  apmul2  8962  ltmul2  9029  lemul2  9030  ltmulgt11  9037  ltmulgt12  9038  gt0div  9043  ge0div  9044  ltmuldiv  9047  ltrec1  9061  lerec2  9062  ledivdiv  9063  ltdiv23  9065  lediv23  9066  suprleubex  9127  creur  9132  creui  9133  nn1suc  9155  nnrecl  9393  znnsub  9524  zgt0ge1  9531  zltlen  9551  nn0n0n1ge2b  9552  nn0le2is012  9555  btwnnz  9567  gtndiv  9568  prime  9572  eluz2  9754  indstr2  9836  negm  9842  nn01to3  9844  qapne  9866  qltlen  9867  qreccl  9869  irrmulap  9875  divlt1lt  9952  divle1le  9953  nnledivrp  9994  xnn0xadd0  10095  xltadd2  10105  xsubge0  10109  xlesubadd  10111  iccid  10153  elioc2  10164  elico2  10165  elicc2  10166  elfz2  10243  fzen  10271  fzsubel  10288  elfzp1  10300  fzpr  10305  fzrevral2  10334  fzrevral3  10335  nn0disj  10366  2ffzeq  10369  fzosplitsni  10474  fvinim0ffz  10480  ioo0  10512  ico0  10514  ioc0  10515  modq0  10584  negqmod0  10586  zmodidfzo  10608  frecuzrdgtcl  10667  nn0ennn  10688  nninfinf  10698  sq11  10867  nn0le2msqd  10974  nn0opth2d  10978  hashen  11039  zfz1isolem1  11097  zfz1iso  11098  csbwrdg  11136  wrdnval  11137  eqwrd  11147  ccat0  11166  ccatws1lenp1bg  11205  swrd0g  11234  swrdspsleq  11241  pfxeq  11270  pfxsuffeqwrdeq  11272  pfxsuff1eqwrdeq  11273  ccatopth2  11291  wrd2ind  11297  2shfti  11385  cjap  11460  cnreim  11532  rexfiuz  11543  rexanuz2  11545  abs00ap  11616  absext  11617  sqabs  11636  abslt  11642  absle  11643  absdiflt  11646  absdifle  11647  lenegsq  11649  minmax  11784  ltmininf  11789  mingeb  11796  xrminmax  11819  xrmin1inf  11821  xrmin2inf  11822  xrltmininf  11824  xrlemininf  11825  clim  11835  clim0c  11840  climrecvg1n  11902  zsumdc  11938  fsum2dlemstep  11988  binomlem  12037  pwm1geoserap1  12062  zproddc  12133  efieq  12289  sin01bnd  12311  cos01bnd  12312  dvdsval2  12344  modm1div  12354  zdvdsdc  12366  modmulconst  12377  dvdsaddr  12391  dvdsabseq  12401  fzocongeq  12412  zeo3  12422  odd2np1  12427  oddp1d2  12444  zob  12445  oddm1d2  12446  nnoddm1d2  12464  divalgb  12479  divalgmod  12481  modremain  12483  bits0  12502  bitsp1e  12506  bitsp1o  12507  bitscmp  12512  bitsinv1lem  12515  gcdn0gt0  12542  bezoutlemstep  12561  dvdssq  12595  nn0seqcvgd  12606  algcvgblem  12614  lcmdvds  12644  lcmgcdeq  12648  coprmdvds  12657  qredeq  12661  congr  12665  isprm2  12682  isprm3  12683  prmdvdsexp  12713  prmdvdsexpb  12714  prmexpb  12716  prmfac1  12717  cncongrprm  12722  oddpwdclemxy  12734  oddpwdclemodd  12737  qnumdenbi  12757  qnumgt0  12763  hashdvds  12786  crth  12789  fermltl  12799  modprminveq  12816  pcpremul  12859  pc2dvds  12896  pcz  12898  prmpwdvds  12921  4sqlem16  12972  oddennn  13006  ctinfomlemom  13041  prdsbasmpt  13356  prdsbasmpt2  13364  mgm1  13446  ismhm  13537  mhmpropd  13542  issubm  13548  issubm2  13549  grpsubrcan  13657  grplactcnv  13678  grp1  13682  eqgval  13803  eqgid  13806  quselbasg  13810  isghm  13823  conjnmzb  13860  iscmn  13873  eqgabl  13910  rngmneg1  13953  rngmneg2  13954  rngpropd  13961  srgen1zr  13994  ringideu  14023  ringpropd  14044  crngpropd  14045  dvdsrd  14101  dvdsr02  14112  opprunitd  14117  crngunit  14118  unitpropdg  14155  rhmunitinv  14185  isnzr2  14191  issubrng  14206  resrhm2b  14256  aprval  14289  islmod  14298  islssm  14364  islssmg  14365  ellspsn  14424  isridl  14511  zrhrhmb  14629  zndvds  14656  znleval  14660  istopg  14716  eltg  14769  eltg2  14770  tgss2  14796  bastop1  14800  bastop2  14801  iscld  14820  isnei  14861  neiint  14862  iscn  14914  iscnp  14916  iscnp3  14920  tgcn  14925  ssidcn  14927  lmbr2  14931  lmbrf  14932  cnnei  14949  cnrest2  14953  eltx  14976  imasnopn  15016  ispsmet  15040  ismet  15061  isxmet  15062  metn0  15095  xmetres2  15096  elbl3ps  15111  elbl3  15112  xblpnfps  15115  xblpnf  15116  elmopn2  15166  metss  15211  bdxmet  15218  metrest  15223  xmetxp  15224  xmetxpbl  15225  metcnp3  15228  metcnp  15229  metcnp2  15230  metcn  15231  txmetcnp  15235  txmetcn  15236  metcnpd  15237  bl2ioo  15267  addcncntoplem  15278  elcncf  15290  elcncf2  15291  ivthdec  15361  ellimc3apf  15377  cnlimcim  15388  dveflem  15443  ply1termlem  15459  sincosq2sgn  15544  sinq12gt0  15547  logltb  15591  ltexp2  15658  wilthlem1  15697  lgsdilem  15749  lgsdir2lem4  15753  lgsdir2  15755  lgsne0  15760  lgsabs1  15761  gausslemma2dlem3  15785  gausslemma2dlem7  15790  lgseisenlem3  15794  lgsquad3  15806  2lgslem1a  15810  2lgslem3c  15817  2lgslem3d  15818  2lgsoddprmlem4  15834  2sqlem7  15843  2sqlem8a  15844  uhgreq12g  15920  isuhgropm  15925  uhgr0e  15926  upgrop  15948  uhgrvtxedgiedgb  15987  isuspgropen  16008  isusgropen  16009  uhgr2edg  16050  vtxd0nedgbfi  16110  1loopgrvd0fi  16117  iswlk  16134  upgriswlkdc  16171  istrl  16194  iseupth  16256  cbvrald  16334  bj-nalset  16440  bj-sels  16459  bj-nnelirr  16498  isomninnlem  16584  iswomninnlem  16603  iswomni0  16605  ismkvnnlem  16606