Theorem bitrd 187

Description: Deduction form of bitri 183. (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 179	. . 3 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
3		bitrd.2	. . . 4 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	3	pm5.74i 179	. . 3 ⊢ ((𝜑 → 𝜒) ↔ (𝜑 → 𝜃))
5	2, 4	bitri 183	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜃))
6	5	pm5.74ri 180	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bitr2d  188  bitr3d  189  bitr4d  190  syl5bb  191  bitrdi  195  3bitrd  213  3bitr2d  215  3bitr3d  217  3bitr4d  219  imbi12d  233  bibi12d  234  sylan9bb  458  anbi12d  465  orbi12d  783  con1biidc  863  pm4.54dc  888  dn1dc  945  dedlem0a  953  xorbi12d  1364  nbbndc  1376  eleq12d  2228  neeq12d  2347  neleq12d  2428  raleqbi1dv  2660  rexeqbi1dv  2661  reueqd  2662  rmoeqd  2663  raleqbidv  2664  rexeqbidv  2665  raleqbidva  2666  rexeqbidva  2667  eueq3dc  2886  sbc19.21g  3005  sbcabel  3018  sbcel1g  3050  sbceq1g  3051  sbcel2g  3052  sbceq2g  3053  sbccsb2g  3061  sbcco3g  3088  sseq12d  3159  raaanlem  3499  sbcssg  3503  ralsng  3599  2ralunsn  3761  csbunig  3780  disjeq12d  3951  breq123d  3979  sbcbr12g  4019  sbcbr1g  4020  sbcbr2g  4021  treq  4068  nalset  4094  exmidsssn  4163  copsex4g  4207  sucelon  4462  posng  4658  csbxpg  4667  sbcrel  4672  csbcnvg  4770  eliniseg  4956  brcodir  4973  csbrng  5047  sbcfung  5194  fneq12d  5262  feq12d  5309  feq123d  5310  sbcfng  5317  sbcfg  5318  f1osng  5455  csbfv12g  5504  funimass4  5519  dmfco  5536  eqfnfv  5565  eqfnfv2  5566  fneqeql2  5576  fvimacnvi  5581  funimass3  5583  fniniseg  5587  rexsupp  5591  unpreima  5592  ralrnmpt  5609  rexrnmpt  5610  dffo3  5614  fmptco  5633  fressnfv  5654  eufnfv  5697  foima2  5702  fnunirn  5717  dff13  5718  f1elima  5723  cocan1  5737  cocan2  5738  fliftel  5743  fliftf  5749  isoresbr  5759  isoini  5768  f1oiso  5776  f1ofveu  5812  mpoeq123dva  5882  ovid  5937  ov  5940  ovg  5959  ovelrn  5969  caovord2d  5990  ofrfval2  6048  offveqb  6051  eqop  6125  reldm  6134  f1od2  6182  mpoxopoveq  6187  mpoxopovel  6188  tpostpos  6211  smoiso  6249  frecabcl  6346  frecsuclem  6353  nnaordr  6457  nnaword  6458  nnaordex  6474  ereq1  6487  brdifun  6507  erth2  6525  qliftfun  6562  brecop  6570  elmapg  6606  elpmg  6609  dom2lem  6717  xpcomco  6771  php5fin  6827  elfi2  6916  supisolem  6952  inflbti  6968  inl11  7009  ismkvnex  7098  mkvprop  7101  exmidfodomrlemreseldju  7135  ltapig  7258  ltmpig  7259  nlt1pig  7261  mulcmpblnq  7288  ltsonq  7318  lt2addnq  7324  lt2mulnq  7325  archnqq  7337  prarloclemarch  7338  ltrnqg  7340  mulcmpblnq0  7364  preqlu  7392  genpdflem  7427  addnqprllem  7447  addnqprulem  7448  addlocprlemgt  7454  appdivnq  7483  mulnqprl  7488  mulnqpru  7489  mullocprlem  7490  distrlem4prl  7504  distrlem4pru  7505  1idprl  7510  1idpru  7511  ltexprlemloc  7527  cauappcvgprlemladdrl  7577  cauappcvgprlemladd  7578  cauappcvgprlem1  7579  archrecnq  7583  caucvgprlemnkj  7586  caucvgprprlemexb  7627  addcmpblnr  7659  lttrsr  7682  ltsosr  7684  ltasrg  7690  mulextsr1  7701  srpospr  7703  caucvgsrlemcau  7713  caucvgsrlemgt1  7715  caucvgsrlemoffres  7720  map2psrprg  7725  ltresr  7759  axcaucvglemres  7819  cnegexlem1  8050  negeu  8066  subadd2  8079  subcan2  8100  addrsub  8246  ltaddneg  8299  ltaddnegr  8300  ltadd1  8304  leadd2  8306  ltsubadd  8307  lesubadd  8309  ltaddsub2  8312  leaddsub2  8314  ltaddpos  8327  lesub2  8332  ltsub2  8334  ltnegcon1  8338  ltnegcon2  8339  lenegcon1  8341  lenegcon2  8342  addge01  8347  addge02  8348  suble0  8351  leaddle0  8352  lesub0  8354  eqord2  8359  sublt0d  8445  recexre  8453  reaplt  8463  reapltxor  8464  reapneg  8472  remulext1  8474  apreim  8478  apcotr  8482  apadd2  8484  addext  8485  apsub1  8517  mulcanap2d  8536  diveqap0  8555  diveqap1  8578  apmul2  8662  ltmul2  8727  lemul2  8728  ltmulgt11  8735  ltmulgt12  8736  gt0div  8741  ge0div  8742  ltmuldiv  8745  ltrec1  8759  lerec2  8760  ledivdiv  8761  ltdiv23  8763  lediv23  8764  suprleubex  8825  creur  8830  creui  8831  nn1suc  8852  nnrecl  9088  znnsub  9218  zgt0ge1  9225  zltlen  9242  nn0n0n1ge2b  9243  nn0le2is012  9246  btwnnz  9258  gtndiv  9259  prime  9263  eluz2  9445  indstr2  9520  negm  9524  nn01to3  9526  qapne  9548  qltlen  9549  qreccl  9551  divlt1lt  9631  divle1le  9632  nnledivrp  9673  xnn0xadd0  9771  xltadd2  9781  xsubge0  9785  xlesubadd  9787  iccid  9829  elioc2  9840  elico2  9841  elicc2  9842  elfz2  9919  fzen  9945  fzsubel  9962  elfzp1  9974  fzpr  9979  fzrevral2  10008  fzrevral3  10009  nn0disj  10037  2ffzeq  10040  fzosplitsni  10134  fvinim0ffz  10140  ioo0  10159  ico0  10161  ioc0  10162  modq0  10228  negqmod0  10230  zmodidfzo  10252  frecuzrdgtcl  10311  nn0ennn  10332  sq11  10491  nn0le2msqd  10593  nn0opth2d  10597  hashen  10658  zfz1isolem1  10711  zfz1iso  10712  2shfti  10731  cjap  10806  cnreim  10878  rexfiuz  10889  rexanuz2  10891  abs00ap  10962  absext  10963  sqabs  10982  abslt  10988  absle  10989  absdiflt  10992  absdifle  10993  lenegsq  10995  minmax  11129  ltmininf  11134  xrminmax  11162  xrmin1inf  11164  xrmin2inf  11165  xrltmininf  11167  xrlemininf  11168  clim  11178  clim0c  11183  climrecvg1n  11245  zsumdc  11281  fsum2dlemstep  11331  binomlem  11380  pwm1geoserap1  11405  zproddc  11476  efieq  11632  sin01bnd  11654  cos01bnd  11655  dvdsval2  11686  modm1div  11696  zdvdsdc  11708  modmulconst  11719  dvdsaddr  11731  dvdsabseq  11739  fzocongeq  11750  zeo3  11759  odd2np1  11764  oddp1d2  11781  zob  11782  oddm1d2  11783  nnoddm1d2  11801  divalgb  11816  divalgmod  11818  modremain  11820  gcdn0gt0  11862  bezoutlemstep  11881  dvdssq  11915  nn0seqcvgd  11918  algcvgblem  11926  lcmdvds  11956  lcmgcdeq  11960  coprmdvds  11969  qredeq  11973  congr  11977  isprm2  11994  isprm3  11995  prmdvdsexp  12023  prmdvdsexpb  12024  prmexpb  12026  prmfac1  12027  cncongrprm  12032  oddpwdclemxy  12044  oddpwdclemodd  12047  qnumdenbi  12067  qnumgt0  12073  hashdvds  12096  crth  12099  fermltl  12109  modprminveq  12125  oddennn  12132  ctinfomlemom  12167  istopg  12408  eltg  12463  eltg2  12464  tgss2  12490  bastop1  12494  bastop2  12495  iscld  12514  isnei  12555  neiint  12556  iscn  12608  iscnp  12610  iscnp3  12614  tgcn  12619  ssidcn  12621  lmbr2  12625  lmbrf  12626  cnnei  12643  cnrest2  12647  eltx  12670  imasnopn  12710  ispsmet  12734  ismet  12755  isxmet  12756  metn0  12789  xmetres2  12790  elbl3ps  12805  elbl3  12806  xblpnfps  12809  xblpnf  12810  elmopn2  12860  metss  12905  bdxmet  12912  metrest  12917  xmetxp  12918  xmetxpbl  12919  metcnp3  12922  metcnp  12923  metcnp2  12924  metcn  12925  txmetcnp  12929  txmetcn  12930  metcnpd  12931  bl2ioo  12953  addcncntoplem  12962  elcncf  12971  elcncf2  12972  ivthdec  13033  ellimc3apf  13040  cnlimcim  13051  dveflem  13098  sincosq2sgn  13159  sinq12gt0  13162  logltb  13206  cbvrald  13373  bj-nalset  13481  bj-sels  13500  bj-nnelirr  13539  isomninnlem  13612  iswomninnlem  13631  iswomni0  13633  ismkvnnlem  13634