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-1 5  ax-2 6  ax-mp 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  syl6bb  195  3bitrd  213  3bitr2d  215  3bitr3d  217  3bitr4d  219  imbi12d  233  bibi12d  234  sylan9bb  451  anbi12d  458  orbi12d  745  con1biidc  812  pm4.54dc  846  dn1dc  909  dedlem0a  917  xorbi12d  1325  nbbndc  1337  eleq12d  2165  neeq12d  2282  neleq12d  2363  raleqbi1dv  2584  rexeqbi1dv  2585  reueqd  2586  rmoeqd  2587  raleqbidv  2588  rexeqbidv  2589  raleqbidva  2590  rexeqbidva  2591  eueq3dc  2803  sbc19.21g  2921  sbcabel  2934  sbcel1g  2964  sbceq1g  2965  sbcel2g  2966  sbceq2g  2967  sbccsb2g  2974  sbcco3g  2999  sseq12d  3070  raaanlem  3407  sbcssg  3411  ralsng  3503  2ralunsn  3664  csbunig  3683  disjeq12d  3853  breq123d  3881  sbcbr12g  3917  sbcbr1g  3918  sbcbr2g  3919  treq  3964  nalset  3990  exmidsssn  4055  copsex4g  4098  sucelon  4348  posng  4539  csbxpg  4548  sbcrel  4553  csbcnvg  4651  eliniseg  4835  brcodir  4852  csbrng  4926  sbcfung  5073  fneq12d  5140  feq12d  5185  feq123d  5186  sbcfng  5193  sbcfg  5194  f1osng  5329  csbfv12g  5375  funimass4  5390  dmfco  5407  eqfnfv  5436  eqfnfv2  5437  fneqeql2  5447  fvimacnvi  5452  funimass3  5454  fniniseg  5458  rexsupp  5462  unpreima  5463  ralrnmpt  5480  rexrnmpt  5481  dffo3  5485  fmptco  5503  fressnfv  5523  eufnfv  5564  foima2  5569  fnunirn  5584  dff13  5585  f1elima  5590  cocan1  5604  cocan2  5605  fliftel  5610  fliftf  5616  isoresbr  5626  isoini  5635  f1oiso  5643  f1ofveu  5678  mpt2eq123dva  5748  ovid  5799  ov  5802  ovg  5821  ovelrn  5831  caovord2d  5852  ofrfval2  5909  offveqb  5912  eqop  5985  reldm  5994  f1od2  6038  mpt2xopoveq  6043  mpt2xopovel  6044  isprmpt2  6046  tpostpos  6067  smoiso  6105  frecabcl  6202  frecsuclem  6209  nnaordr  6309  nnaword  6310  nnaordex  6326  ereq1  6339  brdifun  6359  erth2  6377  qliftfun  6414  brecop  6422  elmapg  6458  elpmg  6461  dom2lem  6569  xpcomco  6622  php5fin  6678  supisolem  6783  inflbti  6799  mkvprop  6901  exmidfodomrlemreseldju  6923  ltapig  6994  ltmpig  6995  nlt1pig  6997  mulcmpblnq  7024  ltsonq  7054  lt2addnq  7060  lt2mulnq  7061  archnqq  7073  prarloclemarch  7074  ltrnqg  7076  mulcmpblnq0  7100  preqlu  7128  genpdflem  7163  addnqprllem  7183  addnqprulem  7184  addlocprlemgt  7190  appdivnq  7219  mulnqprl  7224  mulnqpru  7225  mullocprlem  7226  distrlem4prl  7240  distrlem4pru  7241  1idprl  7246  1idpru  7247  ltexprlemloc  7263  cauappcvgprlemladdrl  7313  cauappcvgprlemladd  7314  cauappcvgprlem1  7315  archrecnq  7319  caucvgprlemnkj  7322  caucvgprprlemexb  7363  addcmpblnr  7382  lttrsr  7405  ltsosr  7407  ltasrg  7413  mulextsr1  7423  srpospr  7425  caucvgsrlemcau  7435  caucvgsrlemgt1  7437  caucvgsrlemoffres  7442  ltresr  7473  axcaucvglemres  7531  cnegexlem1  7754  negeu  7770  subadd2  7783  subcan2  7804  addrsub  7946  ltaddneg  7999  ltaddnegr  8000  ltadd1  8004  leadd2  8006  ltsubadd  8007  lesubadd  8009  ltaddsub2  8012  leaddsub2  8014  ltaddpos  8027  lesub2  8032  ltsub2  8034  ltnegcon1  8038  ltnegcon2  8039  lenegcon1  8041  lenegcon2  8042  addge01  8047  addge02  8048  suble0  8051  leaddle0  8052  lesub0  8054  eqord2  8059  sublt0d  8144  recexre  8152  reaplt  8162  reapltxor  8163  reapneg  8171  remulext1  8173  apreim  8177  apcotr  8181  apadd2  8183  addext  8184  apsub1  8214  mulcanap2d  8228  diveqap0  8246  diveqap1  8269  apmul2  8353  ltmul2  8414  lemul2  8415  ltmulgt11  8422  ltmulgt12  8423  gt0div  8428  ge0div  8429  ltmuldiv  8432  ltrec1  8446  lerec2  8447  ledivdiv  8448  ltdiv23  8450  lediv23  8451  suprleubex  8512  creur  8517  creui  8518  nn1suc  8539  nnrecl  8769  znnsub  8899  zgt0ge1  8906  zltlen  8923  nn0n0n1ge2b  8924  nn0le2is012  8927  btwnnz  8939  gtndiv  8940  prime  8944  eluz2  9124  indstr2  9195  negm  9199  nn01to3  9201  qapne  9223  qltlen  9224  qreccl  9226  divlt1lt  9300  divle1le  9301  nnledivrp  9336  xnn0xadd0  9433  xltadd2  9443  xsubge0  9447  xlesubadd  9449  iccid  9491  elioc2  9502  elico2  9503  elicc2  9504  elfz2  9580  fzen  9606  fzsubel  9623  elfzp1  9635  fzpr  9640  fzrevral2  9669  fzrevral3  9670  nn0disj  9698  2ffzeq  9701  fzosplitsni  9795  fvinim0ffz  9801  ioo0  9820  ico0  9822  ioc0  9823  modq0  9885  negqmod0  9887  zmodidfzo  9909  frecuzrdgtcl  9968  nn0ennn  9989  sq11  10142  nn0le2msqd  10242  nn0opth2d  10246  hashen  10307  zfz1isolem1  10360  zfz1iso  10361  2shfti  10380  cjap  10455  rexfiuz  10537  rexanuz2  10539  abs00ap  10610  absext  10611  sqabs  10630  abslt  10636  absle  10637  absdiflt  10640  absdifle  10641  lenegsq  10643  minmax  10776  ltmininf  10781  xrminmax  10808  xrmin1inf  10810  xrmin2inf  10811  xrltmininf  10813  xrlemininf  10814  clim  10824  clim0c  10829  climrecvg1n  10891  zsumdc  10927  fsum2dlemstep  10977  binomlem  11026  pwm1geoserap1  11051  efieq  11175  sin01bnd  11197  cos01bnd  11198  dvdsval2  11226  zdvdsdc  11244  modmulconst  11255  dvdsaddr  11267  dvdsabseq  11275  fzocongeq  11286  zeo3  11295  odd2np1  11300  oddp1d2  11317  zob  11318  oddm1d2  11319  nnoddm1d2  11337  divalgb  11352  divalgmod  11354  modremain  11356  gcdn0gt0  11396  bezoutlemstep  11413  dvdssq  11447  nn0seqcvgd  11450  algcvgblem  11458  lcmdvds  11488  lcmgcdeq  11492  coprmdvds  11501  qredeq  11505  congr  11509  isprm2  11526  isprm3  11527  prmdvdsexp  11554  prmdvdsexpb  11555  prmexpb  11557  prmfac1  11558  cncongrprm  11563  oddpwdclemxy  11574  oddpwdclemodd  11577  qnumdenbi  11597  qnumgt0  11603  hashdvds  11624  crth  11627  oddennn  11632  istopg  11850  eltg  11904  eltg2  11905  tgss2  11931  bastop1  11935  bastop2  11936  iscld  11955  isnei  11996  neiint  11997  iscn  12048  iscnp  12050  iscnp3  12054  tgcn  12059  ssidcn  12061  lmbr2  12065  lmbrf  12066  cnnei  12083  cnrest2  12087  ispsmet  12109  ismet  12130  isxmet  12131  metn0  12164  xmetres2  12165  elbl3ps  12180  elbl3  12181  xblpnfps  12184  xblpnf  12185  elmopn2  12235  metss  12280  bdxmet  12287  metrest  12292  metcnp3  12293  metcnp  12294  metcnp2  12295  metcn  12296  bl2ioo  12316  elcncf  12326  elcncf2  12327  cbvrald  12396  bj-nalset  12494  bj-sels  12513  bj-nnelirr  12556