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  801  con1biidc  885  pm4.54dc  910  dn1dc  969  dedlem0a  977  dfifp3dc  991  dfifp4dc  992  dfifp5dc  993  3bior2fd  1391  xorbi12d  1427  nbbndc  1439  eleq12d  2305  neeq12d  2434  neleq12d  2515  raleqbi1dv  2755  rexeqbi1dv  2756  reueqd  2757  rmoeqd  2758  raleqbidv  2759  rexeqbidv  2760  raleqbidva  2761  rexeqbidva  2762  eueq3dc  2993  sbc19.21g  3113  sbcabel  3127  sbcel1g  3159  sbceq1g  3160  sbcel2g  3161  sbceq2g  3162  sbccsb2g  3170  sbcco3g  3198  sseq12d  3271  raaanlem  3616  sbcssg  3620  ralsng  3731  2ralunsn  3905  csbunig  3924  disjeq12d  4096  breq123d  4125  sbcbr12g  4167  sbcbr1g  4168  sbcbr2g  4169  treq  4216  nalset  4242  exmidsssn  4317  copsex4g  4365  onsucb  4627  posng  4824  csbxpg  4833  sbcrel  4838  csbcnvg  4941  eliniseg  5134  brcodir  5152  csbrng  5226  sbcfung  5378  fneq12d  5450  feq12d  5500  feq123d  5501  sbcfng  5508  sbcfg  5509  f1osng  5659  csbfv12g  5712  funimass4  5729  dmfco  5747  eqfnfv  5777  eqfnfv2  5778  fneqeql2  5789  fvimacnvi  5794  funimass3  5796  fniniseg  5800  unpreima  5804  ralrnmpt  5821  rexrnmpt  5822  dffo3  5826  fmptco  5845  fressnfv  5873  eufnfv  5919  foima2  5926  fnunirn  5942  dff13  5943  f1elima  5948  cocan1  5962  cocan2  5963  fliftel  5968  fliftf  5974  isoresbr  5984  isoini  5993  f1oiso  6001  f1ofveu  6040  mpoeq123dva  6116  ovid  6172  ov  6175  ovg  6195  ovelrn  6205  caovord2d  6226  ofrfval2  6285  offveqb  6288  eqop  6373  reldm  6382  f1od2  6433  suppval1  6441  suppssrst  6463  suppssrgst  6464  mpoxopoveq  6473  mpoxopovel  6474  tpostpos  6497  smoiso  6535  frecabcl  6632  frecsuclem  6639  nnaordr  6745  nnaword  6746  nnaordex  6763  ereq1  6776  brdifun  6796  erth2  6816  qliftfun  6853  brecop  6861  elmapg  6897  elpmg  6900  mapsnd  6925  dom2lem  7013  xpcomco  7079  pw2f1odclem  7089  php5fin  7141  funisfsupp  7246  ffsuppbi  7255  elfi2  7261  supisolem  7301  inflbti  7317  inl11  7358  ismkvnex  7448  mkvprop  7451  nninfwlporlemd  7465  exmidfodomrlemreseldju  7505  ltapig  7658  ltmpig  7659  nlt1pig  7661  mulcmpblnq  7688  ltsonq  7718  lt2addnq  7724  lt2mulnq  7725  archnqq  7737  prarloclemarch  7738  ltrnqg  7740  mulcmpblnq0  7764  preqlu  7792  genpdflem  7827  addnqprllem  7847  addnqprulem  7848  addlocprlemgt  7854  appdivnq  7883  mulnqprl  7888  mulnqpru  7889  mullocprlem  7890  distrlem4prl  7904  distrlem4pru  7905  1idprl  7910  1idpru  7911  ltexprlemloc  7927  cauappcvgprlemladdrl  7977  cauappcvgprlemladd  7978  cauappcvgprlem1  7979  archrecnq  7983  caucvgprlemnkj  7986  caucvgprprlemexb  8027  addcmpblnr  8059  lttrsr  8082  ltsosr  8084  ltasrg  8090  mulextsr1  8101  srpospr  8103  caucvgsrlemcau  8113  caucvgsrlemgt1  8115  caucvgsrlemoffres  8120  map2psrprg  8125  ltresr  8159  axcaucvglemres  8219  eqlelt  8365  cnegexlem1  8453  negeu  8469  subadd2  8482  subcan2  8503  addrsub  8649  ltaddneg  8703  ltaddnegr  8704  ltadd1  8708  leadd2  8710  ltsubadd  8711  lesubadd  8713  ltaddsub2  8716  leaddsub2  8718  ltaddpos  8731  lesub2  8736  ltsub2  8738  ltnegcon1  8742  ltnegcon2  8743  lenegcon1  8745  lenegcon2  8746  addge01  8751  addge02  8752  suble0  8755  leaddle0  8756  lesub0  8758  eqord2  8763  sublt0d  8849  recexre  8857  reaplt  8867  reapltxor  8868  reapneg  8876  remulext1  8878  apreim  8882  apcotr  8886  apadd2  8888  addext  8889  apsub1  8921  mulcanap2d  8941  diveqap0  8961  diveqap1  8984  apmul2  9068  ltmul2  9135  lemul2  9136  ltmulgt11  9143  ltmulgt12  9144  gt0div  9149  ge0div  9150  ltmuldiv  9153  ltrec1  9167  lerec2  9168  ledivdiv  9169  ltdiv23  9171  lediv23  9172  suprleubex  9233  creur  9238  creui  9239  nn1suc  9261  nnrecl  9499  fcdmnn0fsuppg  9556  znnsub  9634  zgt0ge1  9641  zltlen  9662  nn0n0n1ge2b  9663  nn0le2is012  9666  btwnnz  9678  gtndiv  9679  prime  9683  eluz2  9865  indstr2  9947  negm  9953  nn01to3  9955  qapne  9977  qltlen  9978  qreccl  9980  irrmulap  9986  divlt1lt  10063  divle1le  10064  nnledivrp  10105  xnn0xadd0  10206  xltadd2  10216  xsubge0  10220  xlesubadd  10222  iccid  10264  elioc2  10275  elico2  10276  elicc2  10277  elfz2  10355  fzen  10383  fzsubel  10400  elfzp1  10413  fzpr  10418  fzrevral2  10447  fzrevral3  10448  nn0disj  10479  2ffzeq  10482  fzosplitsni  10588  fvinim0ffz  10594  ioo0  10626  ico0  10628  ioc0  10629  modq0  10698  negqmod0  10700  zmodidfzo  10722  frecuzrdgtcl  10781  nn0ennn  10802  nninfinf  10812  sq11  10981  nn0le2msqd  11089  nn0opth2d  11093  hashen  11155  zfz1isolem1  11220  zfz1iso  11221  csbwrdg  11262  wrdnval  11263  eqwrd  11273  ccat0  11292  ccatws1lenp1bg  11331  swrd0g  11360  swrdspsleq  11367  pfxeq  11396  pfxsuffeqwrdeq  11398  pfxsuff1eqwrdeq  11399  ccatopth2  11417  wrd2ind  11423  2shfti  11524  cjap  11599  cnreim  11671  rexfiuz  11682  rexanuz2  11684  abs00ap  11755  absext  11756  sqabs  11775  abslt  11781  absle  11782  absdiflt  11785  absdifle  11786  lenegsq  11788  minmax  11923  ltmininf  11928  mingeb  11935  xrminmax  11958  xrmin1inf  11960  xrmin2inf  11961  xrltmininf  11963  xrlemininf  11964  clim  11974  clim0c  11979  climrecvg1n  12041  zsumdc  12078  fsum2dlemstep  12128  binomlem  12177  pwm1geoserap1  12202  zproddc  12273  efieq  12429  sin01bnd  12451  cos01bnd  12452  dvdsval2  12484  modm1div  12494  zdvdsdc  12506  modmulconst  12517  dvdsaddr  12531  dvdsabseq  12541  fzocongeq  12552  zeo3  12562  odd2np1  12567  oddp1d2  12584  zob  12585  oddm1d2  12586  nnoddm1d2  12604  divalgb  12619  divalgmod  12621  modremain  12623  bits0  12642  bitsp1e  12646  bitsp1o  12647  bitscmp  12652  bitsinv1lem  12655  gcdn0gt0  12682  bezoutlemstep  12701  dvdssq  12735  nn0seqcvgd  12746  algcvgblem  12754  lcmdvds  12784  lcmgcdeq  12788  coprmdvds  12797  qredeq  12801  congr  12805  isprm2  12822  isprm3  12823  prmdvdsexp  12853  prmdvdsexpb  12854  prmexpb  12856  prmfac1  12857  cncongrprm  12862  oddpwdclemxy  12874  oddpwdclemodd  12877  qnumdenbi  12897  qnumgt0  12903  hashdvds  12926  crth  12929  fermltl  12939  modprminveq  12956  pcpremul  12999  pc2dvds  13036  pcz  13038  prmpwdvds  13061  4sqlem16  13112  ballotfilemfc0  13157  ballotfilemfcc  13158  ballotfilemodife  13162  oddennn  13164  ctinfomlemom  13199  prdsbasmpt  13514  prdsbasmpt2  13522  mgm1  13604  ismhm  13695  mhmpropd  13700  issubm  13706  issubm2  13707  grpsubrcan  13815  grplactcnv  13836  grp1  13840  eqgval  13961  eqgid  13964  quselbasg  13968  isghm  13981  conjnmzb  14018  iscmn  14031  eqgabl  14068  rngmneg1  14112  rngmneg2  14113  rngpropd  14120  srgen1zr  14153  ringideu  14182  ringpropd  14203  crngpropd  14204  dvdsrd  14261  dvdsr02  14272  opprunitd  14277  crngunit  14278  unitpropdg  14315  rhmunitinv  14345  isnzr2  14351  issubrng  14367  resrhm2b  14417  aprval  14451  aprunit  14452  isdrngtap  14466  opprdrng  14480  rngen1zr  14482  islmod  14488  islssm  14554  islssmg  14555  ellspsn  14614  isridl  14701  zrhrhmb  14819  zndvds  14846  znleval  14850  istopg  14913  eltg  14966  eltg2  14967  tgss2  14993  bastop1  14997  bastop2  14998  iscld  15017  isnei  15058  neiint  15059  iscn  15111  iscnp  15113  iscnp3  15117  tgcn  15122  ssidcn  15124  lmbr2  15128  lmbrf  15129  cnnei  15146  cnrest2  15150  eltx  15173  imasnopn  15213  ispsmet  15237  ismet  15258  isxmet  15259  metn0  15292  xmetres2  15293  elbl3ps  15308  elbl3  15309  xblpnfps  15312  xblpnf  15313  elmopn2  15363  metss  15408  bdxmet  15415  metrest  15420  xmetxp  15421  xmetxpbl  15422  metcnp3  15425  metcnp  15426  metcnp2  15427  metcn  15428  txmetcnp  15432  txmetcn  15433  metcnpd  15434  bl2ioo  15464  addcncntoplem  15475  elcncf  15487  elcncf2  15488  ivthdec  15558  ellimc3apf  15574  cnlimcim  15585  dveflem  15640  ply1termlem  15656  sincosq2sgn  15741  sinq12gt0  15744  logltb  15788  ltexp2  15855  wilthlem1  15897  lgsdilem  15949  lgsdir2lem4  15953  lgsdir2  15955  lgsne0  15960  lgsabs1  15961  gausslemma2dlem3  15985  gausslemma2dlem7  15990  lgseisenlem3  15994  lgsquad3  16006  2lgslem1a  16010  2lgslem3c  16017  2lgslem3d  16018  2lgsoddprmlem4  16034  2sqlem7  16043  2sqlem8a  16044  uhgreq12g  16120  isuhgropm  16125  uhgr0e  16126  upgrop  16148  uhgrvtxedgiedgb  16187  isuspgropen  16208  isusgropen  16209  uhgr2edg  16250  issubgr2  16302  uhgrspansubgrlem  16320  vtxd0nedgbfi  16343  1loopgrvd0fi  16350  iswlk  16367  upgriswlkdc  16404  istrl  16429  iseupth  16491  eupth2lem2dc  16503  eupth2lem3lem3fi  16514  eupth2lem3lem4fi  16517  eupth2lem3lem7fi  16518  cbvrald  16609  bj-nalset  16714  bj-sels  16733  bj-nnelirr  16772  isomninnlem  16863  iswomninnlem  16883  iswomni0  16885  ismkvnnlem  16886