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  800  con1biidc  884  pm4.54dc  909  dn1dc  968  dedlem0a  976  dfifp3dc  990  dfifp4dc  991  dfifp5dc  992  3bior2fd  1390  xorbi12d  1426  nbbndc  1438  eleq12d  2301  neeq12d  2421  neleq12d  2502  raleqbi1dv  2741  rexeqbi1dv  2742  reueqd  2743  rmoeqd  2744  raleqbidv  2745  rexeqbidv  2746  raleqbidva  2747  rexeqbidva  2748  eueq3dc  2979  sbc19.21g  3099  sbcabel  3113  sbcel1g  3145  sbceq1g  3146  sbcel2g  3147  sbceq2g  3148  sbccsb2g  3156  sbcco3g  3184  sseq12d  3257  raaanlem  3598  sbcssg  3602  ralsng  3710  2ralunsn  3883  csbunig  3902  disjeq12d  4074  breq123d  4103  sbcbr12g  4145  sbcbr1g  4146  sbcbr2g  4147  treq  4194  nalset  4220  exmidsssn  4294  copsex4g  4341  onsucb  4603  posng  4800  csbxpg  4809  sbcrel  4814  csbcnvg  4916  eliniseg  5108  brcodir  5126  csbrng  5200  sbcfung  5352  fneq12d  5424  feq12d  5474  feq123d  5475  sbcfng  5482  sbcfg  5483  f1osng  5629  csbfv12g  5682  funimass4  5699  dmfco  5717  eqfnfv  5747  eqfnfv2  5748  fneqeql2  5759  fvimacnvi  5764  funimass3  5766  fniniseg  5770  rexsupp  5774  unpreima  5775  ralrnmpt  5792  rexrnmpt  5793  dffo3  5797  fmptco  5816  fressnfv  5844  eufnfv  5890  foima2  5897  fnunirn  5913  dff13  5914  f1elima  5919  cocan1  5933  cocan2  5934  fliftel  5939  fliftf  5945  isoresbr  5955  isoini  5964  f1oiso  5972  f1ofveu  6011  mpoeq123dva  6087  ovid  6143  ov  6146  ovg  6166  ovelrn  6176  caovord2d  6197  ofrfval2  6257  offveqb  6260  eqop  6345  reldm  6354  f1od2  6405  mpoxopoveq  6411  mpoxopovel  6412  tpostpos  6435  smoiso  6473  frecabcl  6570  frecsuclem  6577  nnaordr  6683  nnaword  6684  nnaordex  6701  ereq1  6714  brdifun  6734  erth2  6754  qliftfun  6791  brecop  6799  elmapg  6835  elpmg  6838  dom2lem  6950  xpcomco  7015  pw2f1odclem  7025  php5fin  7076  elfi2  7176  supisolem  7212  inflbti  7228  inl11  7269  ismkvnex  7359  mkvprop  7362  nninfwlporlemd  7376  exmidfodomrlemreseldju  7416  ltapig  7563  ltmpig  7564  nlt1pig  7566  mulcmpblnq  7593  ltsonq  7623  lt2addnq  7629  lt2mulnq  7630  archnqq  7642  prarloclemarch  7643  ltrnqg  7645  mulcmpblnq0  7669  preqlu  7697  genpdflem  7732  addnqprllem  7752  addnqprulem  7753  addlocprlemgt  7759  appdivnq  7788  mulnqprl  7793  mulnqpru  7794  mullocprlem  7795  distrlem4prl  7809  distrlem4pru  7810  1idprl  7815  1idpru  7816  ltexprlemloc  7832  cauappcvgprlemladdrl  7882  cauappcvgprlemladd  7883  cauappcvgprlem1  7884  archrecnq  7888  caucvgprlemnkj  7891  caucvgprprlemexb  7932  addcmpblnr  7964  lttrsr  7987  ltsosr  7989  ltasrg  7995  mulextsr1  8006  srpospr  8008  caucvgsrlemcau  8018  caucvgsrlemgt1  8020  caucvgsrlemoffres  8025  map2psrprg  8030  ltresr  8064  axcaucvglemres  8124  eqlelt  8271  cnegexlem1  8359  negeu  8375  subadd2  8388  subcan2  8409  addrsub  8555  ltaddneg  8609  ltaddnegr  8610  ltadd1  8614  leadd2  8616  ltsubadd  8617  lesubadd  8619  ltaddsub2  8622  leaddsub2  8624  ltaddpos  8637  lesub2  8642  ltsub2  8644  ltnegcon1  8648  ltnegcon2  8649  lenegcon1  8651  lenegcon2  8652  addge01  8657  addge02  8658  suble0  8661  leaddle0  8662  lesub0  8664  eqord2  8669  sublt0d  8755  recexre  8763  reaplt  8773  reapltxor  8774  reapneg  8782  remulext1  8784  apreim  8788  apcotr  8792  apadd2  8794  addext  8795  apsub1  8827  mulcanap2d  8847  diveqap0  8867  diveqap1  8890  apmul2  8974  ltmul2  9041  lemul2  9042  ltmulgt11  9049  ltmulgt12  9050  gt0div  9055  ge0div  9056  ltmuldiv  9059  ltrec1  9073  lerec2  9074  ledivdiv  9075  ltdiv23  9077  lediv23  9078  suprleubex  9139  creur  9144  creui  9145  nn1suc  9167  nnrecl  9405  znnsub  9536  zgt0ge1  9543  zltlen  9563  nn0n0n1ge2b  9564  nn0le2is012  9567  btwnnz  9579  gtndiv  9580  prime  9584  eluz2  9766  indstr2  9848  negm  9854  nn01to3  9856  qapne  9878  qltlen  9879  qreccl  9881  irrmulap  9887  divlt1lt  9964  divle1le  9965  nnledivrp  10006  xnn0xadd0  10107  xltadd2  10117  xsubge0  10121  xlesubadd  10123  iccid  10165  elioc2  10176  elico2  10177  elicc2  10178  elfz2  10255  fzen  10283  fzsubel  10300  elfzp1  10312  fzpr  10317  fzrevral2  10346  fzrevral3  10347  nn0disj  10378  2ffzeq  10381  fzosplitsni  10487  fvinim0ffz  10493  ioo0  10525  ico0  10527  ioc0  10528  modq0  10597  negqmod0  10599  zmodidfzo  10621  frecuzrdgtcl  10680  nn0ennn  10701  nninfinf  10711  sq11  10880  nn0le2msqd  10987  nn0opth2d  10991  hashen  11052  zfz1isolem1  11110  zfz1iso  11111  csbwrdg  11152  wrdnval  11153  eqwrd  11163  ccat0  11182  ccatws1lenp1bg  11221  swrd0g  11250  swrdspsleq  11257  pfxeq  11286  pfxsuffeqwrdeq  11288  pfxsuff1eqwrdeq  11289  ccatopth2  11307  wrd2ind  11313  2shfti  11414  cjap  11489  cnreim  11561  rexfiuz  11572  rexanuz2  11574  abs00ap  11645  absext  11646  sqabs  11665  abslt  11671  absle  11672  absdiflt  11675  absdifle  11676  lenegsq  11678  minmax  11813  ltmininf  11818  mingeb  11825  xrminmax  11848  xrmin1inf  11850  xrmin2inf  11851  xrltmininf  11853  xrlemininf  11854  clim  11864  clim0c  11869  climrecvg1n  11931  zsumdc  11968  fsum2dlemstep  12018  binomlem  12067  pwm1geoserap1  12092  zproddc  12163  efieq  12319  sin01bnd  12341  cos01bnd  12342  dvdsval2  12374  modm1div  12384  zdvdsdc  12396  modmulconst  12407  dvdsaddr  12421  dvdsabseq  12431  fzocongeq  12442  zeo3  12452  odd2np1  12457  oddp1d2  12474  zob  12475  oddm1d2  12476  nnoddm1d2  12494  divalgb  12509  divalgmod  12511  modremain  12513  bits0  12532  bitsp1e  12536  bitsp1o  12537  bitscmp  12542  bitsinv1lem  12545  gcdn0gt0  12572  bezoutlemstep  12591  dvdssq  12625  nn0seqcvgd  12636  algcvgblem  12644  lcmdvds  12674  lcmgcdeq  12678  coprmdvds  12687  qredeq  12691  congr  12695  isprm2  12712  isprm3  12713  prmdvdsexp  12743  prmdvdsexpb  12744  prmexpb  12746  prmfac1  12747  cncongrprm  12752  oddpwdclemxy  12764  oddpwdclemodd  12767  qnumdenbi  12787  qnumgt0  12793  hashdvds  12816  crth  12819  fermltl  12829  modprminveq  12846  pcpremul  12889  pc2dvds  12926  pcz  12928  prmpwdvds  12951  4sqlem16  13002  oddennn  13036  ctinfomlemom  13071  prdsbasmpt  13386  prdsbasmpt2  13394  mgm1  13476  ismhm  13567  mhmpropd  13572  issubm  13578  issubm2  13579  grpsubrcan  13687  grplactcnv  13708  grp1  13712  eqgval  13833  eqgid  13836  quselbasg  13840  isghm  13853  conjnmzb  13890  iscmn  13903  eqgabl  13940  rngmneg1  13984  rngmneg2  13985  rngpropd  13992  srgen1zr  14025  ringideu  14054  ringpropd  14075  crngpropd  14076  dvdsrd  14132  dvdsr02  14143  opprunitd  14148  crngunit  14149  unitpropdg  14186  rhmunitinv  14216  isnzr2  14222  issubrng  14237  resrhm2b  14287  aprval  14320  islmod  14329  islssm  14395  islssmg  14396  ellspsn  14455  isridl  14542  zrhrhmb  14660  zndvds  14687  znleval  14691  istopg  14752  eltg  14805  eltg2  14806  tgss2  14832  bastop1  14836  bastop2  14837  iscld  14856  isnei  14897  neiint  14898  iscn  14950  iscnp  14952  iscnp3  14956  tgcn  14961  ssidcn  14963  lmbr2  14967  lmbrf  14968  cnnei  14985  cnrest2  14989  eltx  15012  imasnopn  15052  ispsmet  15076  ismet  15097  isxmet  15098  metn0  15131  xmetres2  15132  elbl3ps  15147  elbl3  15148  xblpnfps  15151  xblpnf  15152  elmopn2  15202  metss  15247  bdxmet  15254  metrest  15259  xmetxp  15260  xmetxpbl  15261  metcnp3  15264  metcnp  15265  metcnp2  15266  metcn  15267  txmetcnp  15271  txmetcn  15272  metcnpd  15273  bl2ioo  15303  addcncntoplem  15314  elcncf  15326  elcncf2  15327  ivthdec  15397  ellimc3apf  15413  cnlimcim  15424  dveflem  15479  ply1termlem  15495  sincosq2sgn  15580  sinq12gt0  15583  logltb  15627  ltexp2  15694  wilthlem1  15733  lgsdilem  15785  lgsdir2lem4  15789  lgsdir2  15791  lgsne0  15796  lgsabs1  15797  gausslemma2dlem3  15821  gausslemma2dlem7  15826  lgseisenlem3  15830  lgsquad3  15842  2lgslem1a  15846  2lgslem3c  15853  2lgslem3d  15854  2lgsoddprmlem4  15870  2sqlem7  15879  2sqlem8a  15880  uhgreq12g  15956  isuhgropm  15961  uhgr0e  15962  upgrop  15984  uhgrvtxedgiedgb  16023  isuspgropen  16044  isusgropen  16045  uhgr2edg  16086  issubgr2  16138  uhgrspansubgrlem  16156  vtxd0nedgbfi  16179  1loopgrvd0fi  16186  iswlk  16203  upgriswlkdc  16240  istrl  16265  iseupth  16327  eupth2lem2dc  16339  eupth2lem3lem3fi  16350  eupth2lem3lem4fi  16353  eupth2lem3lem7fi  16354  cbvrald  16445  bj-nalset  16550  bj-sels  16569  bj-nnelirr  16608  isomninnlem  16701  iswomninnlem  16721  iswomni0  16723  ismkvnnlem  16724