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  797  con1biidc  881  pm4.54dc  906  dn1dc  965  dedlem0a  973  3bior2fd  1368  xorbi12d  1404  nbbndc  1416  eleq12d  2280  neeq12d  2400  neleq12d  2481  raleqbi1dv  2720  rexeqbi1dv  2721  reueqd  2722  rmoeqd  2723  raleqbidv  2724  rexeqbidv  2725  raleqbidva  2726  rexeqbidva  2727  eueq3dc  2957  sbc19.21g  3077  sbcabel  3091  sbcel1g  3123  sbceq1g  3124  sbcel2g  3125  sbceq2g  3126  sbccsb2g  3134  sbcco3g  3162  sseq12d  3235  raaanlem  3576  sbcssg  3580  ralsng  3686  2ralunsn  3856  csbunig  3875  disjeq12d  4047  breq123d  4076  sbcbr12g  4118  sbcbr1g  4119  sbcbr2g  4120  treq  4167  nalset  4193  exmidsssn  4265  copsex4g  4312  onsucb  4572  posng  4768  csbxpg  4777  sbcrel  4782  csbcnvg  4883  eliniseg  5074  brcodir  5092  csbrng  5166  sbcfung  5318  fneq12d  5389  feq12d  5439  feq123d  5440  sbcfng  5447  sbcfg  5448  f1osng  5590  csbfv12g  5641  funimass4  5657  dmfco  5675  eqfnfv  5705  eqfnfv2  5706  fneqeql2  5717  fvimacnvi  5722  funimass3  5724  fniniseg  5728  rexsupp  5732  unpreima  5733  ralrnmpt  5750  rexrnmpt  5751  dffo3  5755  fmptco  5774  fressnfv  5799  eufnfv  5843  foima2  5848  fnunirn  5864  dff13  5865  f1elima  5870  cocan1  5884  cocan2  5885  fliftel  5890  fliftf  5896  isoresbr  5906  isoini  5915  f1oiso  5923  f1ofveu  5962  mpoeq123dva  6036  ovid  6092  ov  6095  ovg  6115  ovelrn  6125  caovord2d  6146  ofrfval2  6205  offveqb  6208  eqop  6293  reldm  6302  f1od2  6351  mpoxopoveq  6356  mpoxopovel  6357  tpostpos  6380  smoiso  6418  frecabcl  6515  frecsuclem  6522  nnaordr  6626  nnaword  6627  nnaordex  6644  ereq1  6657  brdifun  6677  erth2  6697  qliftfun  6734  brecop  6742  elmapg  6778  elpmg  6781  dom2lem  6893  xpcomco  6953  pw2f1odclem  6963  php5fin  7012  elfi2  7107  supisolem  7143  inflbti  7159  inl11  7200  ismkvnex  7290  mkvprop  7293  nninfwlporlemd  7307  exmidfodomrlemreseldju  7346  ltapig  7493  ltmpig  7494  nlt1pig  7496  mulcmpblnq  7523  ltsonq  7553  lt2addnq  7559  lt2mulnq  7560  archnqq  7572  prarloclemarch  7573  ltrnqg  7575  mulcmpblnq0  7599  preqlu  7627  genpdflem  7662  addnqprllem  7682  addnqprulem  7683  addlocprlemgt  7689  appdivnq  7718  mulnqprl  7723  mulnqpru  7724  mullocprlem  7725  distrlem4prl  7739  distrlem4pru  7740  1idprl  7745  1idpru  7746  ltexprlemloc  7762  cauappcvgprlemladdrl  7812  cauappcvgprlemladd  7813  cauappcvgprlem1  7814  archrecnq  7818  caucvgprlemnkj  7821  caucvgprprlemexb  7862  addcmpblnr  7894  lttrsr  7917  ltsosr  7919  ltasrg  7925  mulextsr1  7936  srpospr  7938  caucvgsrlemcau  7948  caucvgsrlemgt1  7950  caucvgsrlemoffres  7955  map2psrprg  7960  ltresr  7994  axcaucvglemres  8054  eqlelt  8201  cnegexlem1  8289  negeu  8305  subadd2  8318  subcan2  8339  addrsub  8485  ltaddneg  8539  ltaddnegr  8540  ltadd1  8544  leadd2  8546  ltsubadd  8547  lesubadd  8549  ltaddsub2  8552  leaddsub2  8554  ltaddpos  8567  lesub2  8572  ltsub2  8574  ltnegcon1  8578  ltnegcon2  8579  lenegcon1  8581  lenegcon2  8582  addge01  8587  addge02  8588  suble0  8591  leaddle0  8592  lesub0  8594  eqord2  8599  sublt0d  8685  recexre  8693  reaplt  8703  reapltxor  8704  reapneg  8712  remulext1  8714  apreim  8718  apcotr  8722  apadd2  8724  addext  8725  apsub1  8757  mulcanap2d  8777  diveqap0  8797  diveqap1  8820  apmul2  8904  ltmul2  8971  lemul2  8972  ltmulgt11  8979  ltmulgt12  8980  gt0div  8985  ge0div  8986  ltmuldiv  8989  ltrec1  9003  lerec2  9004  ledivdiv  9005  ltdiv23  9007  lediv23  9008  suprleubex  9069  creur  9074  creui  9075  nn1suc  9097  nnrecl  9335  znnsub  9466  zgt0ge1  9473  zltlen  9493  nn0n0n1ge2b  9494  nn0le2is012  9497  btwnnz  9509  gtndiv  9510  prime  9514  eluz2  9696  indstr2  9772  negm  9778  nn01to3  9780  qapne  9802  qltlen  9803  qreccl  9805  irrmulap  9811  divlt1lt  9888  divle1le  9889  nnledivrp  9930  xnn0xadd0  10031  xltadd2  10041  xsubge0  10045  xlesubadd  10047  iccid  10089  elioc2  10100  elico2  10101  elicc2  10102  elfz2  10179  fzen  10207  fzsubel  10224  elfzp1  10236  fzpr  10241  fzrevral2  10270  fzrevral3  10271  nn0disj  10302  2ffzeq  10305  fzosplitsni  10408  fvinim0ffz  10414  ioo0  10446  ico0  10448  ioc0  10449  modq0  10518  negqmod0  10520  zmodidfzo  10542  frecuzrdgtcl  10601  nn0ennn  10622  nninfinf  10632  sq11  10801  nn0le2msqd  10908  nn0opth2d  10912  hashen  10973  zfz1isolem1  11029  zfz1iso  11030  csbwrdg  11067  wrdnval  11068  eqwrd  11078  ccat0  11097  ccatws1lenp1bg  11134  swrd0g  11158  swrdspsleq  11165  pfxeq  11194  pfxsuffeqwrdeq  11196  pfxsuff1eqwrdeq  11197  ccatopth2  11215  wrd2ind  11221  2shfti  11308  cjap  11383  cnreim  11455  rexfiuz  11466  rexanuz2  11468  abs00ap  11539  absext  11540  sqabs  11559  abslt  11565  absle  11566  absdiflt  11569  absdifle  11570  lenegsq  11572  minmax  11707  ltmininf  11712  mingeb  11719  xrminmax  11742  xrmin1inf  11744  xrmin2inf  11745  xrltmininf  11747  xrlemininf  11748  clim  11758  clim0c  11763  climrecvg1n  11825  zsumdc  11861  fsum2dlemstep  11911  binomlem  11960  pwm1geoserap1  11985  zproddc  12056  efieq  12212  sin01bnd  12234  cos01bnd  12235  dvdsval2  12267  modm1div  12277  zdvdsdc  12289  modmulconst  12300  dvdsaddr  12314  dvdsabseq  12324  fzocongeq  12335  zeo3  12345  odd2np1  12350  oddp1d2  12367  zob  12368  oddm1d2  12369  nnoddm1d2  12387  divalgb  12402  divalgmod  12404  modremain  12406  bits0  12425  bitsp1e  12429  bitsp1o  12430  bitscmp  12435  bitsinv1lem  12438  gcdn0gt0  12465  bezoutlemstep  12484  dvdssq  12518  nn0seqcvgd  12529  algcvgblem  12537  lcmdvds  12567  lcmgcdeq  12571  coprmdvds  12580  qredeq  12584  congr  12588  isprm2  12605  isprm3  12606  prmdvdsexp  12636  prmdvdsexpb  12637  prmexpb  12639  prmfac1  12640  cncongrprm  12645  oddpwdclemxy  12657  oddpwdclemodd  12660  qnumdenbi  12680  qnumgt0  12686  hashdvds  12709  crth  12712  fermltl  12722  modprminveq  12739  pcpremul  12782  pc2dvds  12819  pcz  12821  prmpwdvds  12844  4sqlem16  12895  oddennn  12929  ctinfomlemom  12964  prdsbasmpt  13279  prdsbasmpt2  13287  mgm1  13369  ismhm  13460  mhmpropd  13465  issubm  13471  issubm2  13472  grpsubrcan  13580  grplactcnv  13601  grp1  13605  eqgval  13726  eqgid  13729  quselbasg  13733  isghm  13746  conjnmzb  13783  iscmn  13796  eqgabl  13833  rngmneg1  13876  rngmneg2  13877  rngpropd  13884  srgen1zr  13917  ringideu  13946  ringpropd  13967  crngpropd  13968  dvdsrd  14023  dvdsr02  14034  opprunitd  14039  crngunit  14040  unitpropdg  14077  rhmunitinv  14107  isnzr2  14113  issubrng  14128  resrhm2b  14178  aprval  14211  islmod  14220  islssm  14286  islssmg  14287  ellspsn  14346  isridl  14433  zrhrhmb  14551  zndvds  14578  znleval  14582  istopg  14638  eltg  14691  eltg2  14692  tgss2  14718  bastop1  14722  bastop2  14723  iscld  14742  isnei  14783  neiint  14784  iscn  14836  iscnp  14838  iscnp3  14842  tgcn  14847  ssidcn  14849  lmbr2  14853  lmbrf  14854  cnnei  14871  cnrest2  14875  eltx  14898  imasnopn  14938  ispsmet  14962  ismet  14983  isxmet  14984  metn0  15017  xmetres2  15018  elbl3ps  15033  elbl3  15034  xblpnfps  15037  xblpnf  15038  elmopn2  15088  metss  15133  bdxmet  15140  metrest  15145  xmetxp  15146  xmetxpbl  15147  metcnp3  15150  metcnp  15151  metcnp2  15152  metcn  15153  txmetcnp  15157  txmetcn  15158  metcnpd  15159  bl2ioo  15189  addcncntoplem  15200  elcncf  15212  elcncf2  15213  ivthdec  15283  ellimc3apf  15299  cnlimcim  15310  dveflem  15365  ply1termlem  15381  sincosq2sgn  15466  sinq12gt0  15469  logltb  15513  ltexp2  15580  wilthlem1  15619  lgsdilem  15671  lgsdir2lem4  15675  lgsdir2  15677  lgsne0  15682  lgsabs1  15683  gausslemma2dlem3  15707  gausslemma2dlem7  15712  lgseisenlem3  15716  lgsquad3  15728  2lgslem1a  15732  2lgslem3c  15739  2lgslem3d  15740  2lgsoddprmlem4  15756  2sqlem7  15765  2sqlem8a  15766  uhgreq12g  15841  isuhgropm  15846  uhgr0e  15847  upgrop  15869  uhgrvtxedgiedgb  15906  isuspgropen  15927  isusgropen  15928  uhgr2edg  15969  cbvrald  16062  bj-nalset  16168  bj-sels  16187  bj-nnelirr  16226  isomninnlem  16309  iswomninnlem  16328  iswomni0  16330  ismkvnnlem  16331