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 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bitr2d  189  bitr3d  190  bitr4d  191  bitrid  192  bitrdi  196  3bitrd  214  3bitr2d  216  3bitr3d  218  3bitr4d  220  imbi12d  234  bibi12d  235  sylan9bb  466  anbi12d  477  orbi12d  805  con1biidc  889  pm4.54dc  914  dn1dc  973  dedlem0a  981  dfifp3dc  995  dfifp4dc  996  dfifp5dc  997  3bior2fd  1395  xorbi12d  1431  nbbndc  1443  eleq12d  2309  neeq12d  2440  neleq12d  2521  raleqbi1dv  2761  rexeqbi1dv  2762  reueqd  2763  rmoeqd  2764  raleqbidv  2765  rexeqbidv  2766  raleqbidva  2767  rexeqbidva  2768  eueq3dc  3000  sbc19.21g  3120  sbcabel  3134  sbcel1g  3166  sbceq1g  3167  sbcel2g  3168  sbceq2g  3169  sbccsb2g  3177  sbcco3g  3205  sseq12d  3279  raaanlem  3632  sbcssg  3636  ralsng  3749  2ralunsn  3924  csbunig  3943  disjeq12d  4115  breq123d  4145  sbcbr12g  4187  sbcbr1g  4188  sbcbr2g  4189  treq  4237  nalset  4265  exmidsssn  4341  copsex4g  4389  onsucb  4652  posng  4849  csbxpg  4858  sbcrel  4863  csbcnvg  4966  eliniseg  5160  brcodir  5178  csbrng  5252  sbcfung  5404  fneq12d  5476  feq12d  5526  feq123d  5527  sbcfng  5534  sbcfg  5535  f1osng  5685  csbfv12g  5739  funimass4  5756  dmfco  5776  eqfnfv  5809  eqfnfv2  5810  fneqeql2  5821  fvimacnvi  5826  funimass3  5828  fniniseg  5832  unpreima  5836  ralrnmpt  5853  rexrnmpt  5854  dffo3  5858  fmptco  5877  fressnfv  5905  eufnfv  5952  foima2  5960  fnunirn  5976  dff13  5977  f1elima  5982  cocan1  5996  cocan2  5997  fliftel  6002  fliftf  6008  isoresbr  6018  isoini  6027  f1oiso  6035  f1ofveu  6076  mpoeq123dva  6152  ovid  6208  ov  6211  ovg  6231  ovelrn  6241  caovord2d  6262  ofrfval2  6323  offveqb  6326  eqop  6415  reldm  6424  f1od2  6475  suppval1  6483  suppssrst  6505  suppssrgst  6506  mpoxopoveq  6516  mpoxopovel  6517  tpostpos  6540  smoiso  6578  frecabcl  6675  frecsuclem  6682  nnaordr  6788  nnaword  6789  nnaordex  6806  ereq1  6819  brdifun  6839  erth2  6859  qliftfun  6896  brecop  6904  elmapg  6940  elpmg  6943  mapsnd  6976  dom2lem  7064  xpcomco  7130  pw2f1odclem  7140  php5fin  7192  elfi2  7312  supisolem  7355  inflbti  7371  inl11  7412  ismkvnex  7502  mkvprop  7505  nninfwlporlemd  7519  exmidfodomrlemreseldju  7559  ltapig  7712  ltmpig  7713  nlt1pig  7715  mulcmpblnq  7742  ltsonq  7772  lt2addnq  7778  lt2mulnq  7779  archnqq  7791  prarloclemarch  7792  ltrnqg  7794  mulcmpblnq0  7818  preqlu  7846  genpdflem  7881  addnqprllem  7901  addnqprulem  7902  addlocprlemgt  7908  appdivnq  7937  mulnqprl  7942  mulnqpru  7943  mullocprlem  7944  distrlem4prl  7958  distrlem4pru  7959  1idprl  7964  1idpru  7965  ltexprlemloc  7981  cauappcvgprlemladdrl  8031  cauappcvgprlemladd  8032  cauappcvgprlem1  8033  archrecnq  8037  caucvgprlemnkj  8040  caucvgprprlemexb  8081  addcmpblnr  8113  lttrsr  8136  ltsosr  8138  ltasrg  8144  mulextsr1  8155  srpospr  8157  caucvgsrlemcau  8167  caucvgsrlemgt1  8169  caucvgsrlemoffres  8174  map2psrprg  8179  ltresr  8213  axcaucvglemres  8273  eqlelt  8419  cnegexlem1  8509  negeu  8525  subadd2  8538  subcan2  8559  addrsub  8705  ltaddneg  8760  ltaddnegr  8761  ltadd1  8765  leadd2  8767  ltsubadd  8768  lesubadd  8770  ltaddsub2  8773  leaddsub2  8775  ltaddpos  8788  lesub2  8793  ltsub2  8795  ltnegcon1  8799  ltnegcon2  8800  lenegcon1  8802  lenegcon2  8803  addge01  8808  addge02  8809  suble0  8812  leaddle0  8813  lesub0  8815  eqord2  8820  sublt0d  8907  recexre  8915  reaplt  8925  reapltxor  8926  reapneg  8934  remulext1  8936  apreim  8940  apcotr  8944  apadd2  8946  addext  8947  apsub1  8979  mulcanap2d  8999  diveqap0  9021  diveqap1  9044  apmul2  9128  ltmul2  9195  lemul2  9196  ltmulgt11  9203  ltmulgt12  9204  gt0div  9209  ge0div  9210  ltmuldiv  9213  ltrec1  9227  lerec2  9228  ledivdiv  9229  ltdiv23  9231  lediv23  9232  suprleubex  9293  creur  9298  creui  9299  ofsubeq0  9301  nn1suc  9333  nnrecl  9573  znnsub  9706  zgt0ge1  9713  zltlen  9734  nn0n0n1ge2b  9735  nn0le2is012  9738  fcdmnn0fsuppfi  9744  btwnnz  9751  gtndiv  9752  prime  9756  eluz2  9943  indstr2  10025  negm  10031  nn01to3  10033  qapne  10055  qltlen  10056  qreccl  10058  irrmulap  10065  divlt1lt  10142  divle1le  10143  nnledivrp  10184  xnn0xadd0  10286  xltadd2  10296  xsubge0  10300  xlesubadd  10302  iccid  10344  elioc2  10355  elico2  10356  elicc2  10357  elfz2  10435  fzen  10464  fzsubel  10483  elfzp1  10496  fzpr  10501  fzrevral2  10530  fzrevral3  10531  nn0disj  10562  2ffzeq  10565  fzosplitsni  10671  fvinim0ffz  10677  ioo0  10711  ico0  10713  ioc0  10714  modq0  10787  negqmod0  10789  zmodidfzo  10811  frecuzrdgtcl  10870  nn0ennn  10891  nninfinf  10901  sq11  11070  nn0le2msqd  11179  nn0opth2d  11183  hashen  11245  zfz1isolem1  11314  zfz1iso  11315  csbwrdg  11356  wrdnval  11357  eqwrd  11367  ccat0  11386  ccatws1lenp1bg  11425  swrd0g  11454  swrdspsleq  11461  pfxeq  11490  pfxsuffeqwrdeq  11492  pfxsuff1eqwrdeq  11493  ccatopth2  11511  wrd2ind  11517  2shfti  11618  cjap  11694  cnreim  11766  rexfiuz  11777  rexanuz2  11779  abs00ap  11850  absext  11851  sqabs  11871  abslt  11877  absle  11878  absdiflt  11881  absdifle  11882  lenegsq  11884  minmax  12020  ltmininf  12025  mingeb  12033  xrminmax  12056  xrmin1inf  12058  xrmin2inf  12059  xrltmininf  12061  xrlemininf  12062  clim  12072  clim0c  12077  climrecvg1n  12139  zsumdc  12176  fsum2dlemstep  12226  binomlem  12275  pwm1geoserap1  12300  zproddc  12371  efieq  12527  sin01bnd  12549  cos01bnd  12550  dvdsval2  12582  modm1div  12592  zdvdsdc  12604  modmulconst  12615  dvdsaddr  12629  dvdsabseq  12639  fzocongeq  12650  zeo3  12660  odd2np1  12665  oddp1d2  12682  zob  12683  oddm1d2  12684  nnoddm1d2  12702  divalgb  12717  divalgmod  12719  modremain  12721  bits0  12740  bitsp1e  12744  bitsp1o  12745  bitscmp  12750  bitsinv1lem  12753  gcdn0gt0  12780  bezoutlemstep  12799  dvdssq  12833  nn0seqcvgd  12844  algcvgblem  12852  lcmdvds  12882  lcmgcdeq  12886  coprmdvds  12895  qredeq  12899  congr  12903  isprm2  12920  isprm3  12921  prmdvdsexp  12952  prmdvdsexpb  12953  prmexpb  12955  prmfac1  12956  cncongrprm  12961  nnmaxpwlemxy  12973  nnmaxpwlemnfac  12976  qnumdenbi  12997  qnumgt0  13003  hashdvds  13028  crth  13031  fermltl  13041  modprminveq  13058  pcpremul  13101  pc2dvds  13138  pcz  13140  prmpwdvds  13163  4sqlem16  13214  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemodife  13298  ballotfilemrv1  13322  ballotfilemrv2  13323  ballotfilem1ri  13336  oddennn  13341  ctinfomlemom  13376  mgm1  13749  ismhm  13827  mhmpropd  13832  issubm  13838  issubm2  13839  grpsubrcan  13945  grplactcnv  13966  grp1  13970  eqgval  14085  eqgid  14088  quselbasg  14092  isghm  14105  conjnmzb  14142  iscmn  14186  eqgabl  14224  prdsbasmpt  14287  prdsbasmpt2  14295  rngmneg1  14353  rngmneg2  14354  rngpropd  14361  rngen1zr  14367  srgen1zr0  14399  ringideu  14428  ringpropd  14450  crngpropd  14451  dvdsrd  14510  dvdsr02  14521  opprunitd  14526  crngunit  14527  unitpropdg  14564  rhmunitinv  14594  isnzr2  14600  issubrng  14616  resrhm2b  14666  aprval  14700  aprunit  14701  isdrngtap  14715  opprdrng  14729  islmod  14736  islssm  14803  islssmg  14804  ellspsn  14863  isridl  14950  zrhrhmb  15066  zndvds  15093  znleval  15097  isassa  15111  istopg  15258  eltg  15311  eltg2  15312  tgss2  15338  bastop1  15342  bastop2  15343  iscld  15362  isnei  15403  neiint  15404  iscn  15456  iscnp  15458  iscnp3  15462  tgcn  15467  ssidcn  15469  lmbr2  15473  lmbrf  15474  cnnei  15491  cnrest2  15495  eltx  15518  imasnopn  15558  ispsmet  15582  ismet  15603  isxmet  15604  metn0  15637  xmetres2  15638  elbl3ps  15653  elbl3  15654  xblpnfps  15657  xblpnf  15658  elmopn2  15708  metss  15753  bdxmet  15760  metrest  15765  xmetxp  15766  xmetxpbl  15767  metcnp3  15770  metcnp  15771  metcnp2  15772  metcn  15773  txmetcnp  15777  txmetcn  15778  metcnpd  15779  bl2ioo  15809  addcncntoplem  15820  elcncf  15832  elcncf2  15833  ivthdec  15903  ellimc3apf  15919  cnlimcim  15930  dveflem  15985  ply1termlem  16001  sincosq2sgn  16087  sinq12gt0  16090  logltb  16137  ltexp2  16210  birthdaylem3  16260  wilthlem1  16265  ppiublem1  16324  prmefexple  16341  bposlem1  16344  bposlem6  16349  bposlem7  16350  lgsdilem  16384  lgsdir2lem4  16388  lgsdir2  16390  lgsne0  16395  lgsabs1  16396  gausslemma2dlem3  16420  gausslemma2dlem7  16425  lgseisenlem3  16429  lgsquad3  16441  2lgslem1a  16445  2lgslem3c  16452  2lgslem3d  16453  2lgsoddprmlem4  16469  2sqlem7  16478  2sqlem8a  16479  uhgreq12g  16555  isuhgropm  16560  uhgr0e  16561  upgrop  16583  uhgrvtxedgiedgb  16622  isuspgropen  16643  isusgropen  16644  uhgr2edg  16685  issubgr2  16737  uhgrspansubgrlem  16755  vtxd0nedgbfi  16778  1loopgrvd0fi  16785  iswlk  16802  upgriswlkdc  16839  istrl  16864  iseupth  16926  eupth2lem2dc  16938  eupth2lem3lem3fi  16949  eupth2lem3lem4fi  16952  eupth2lem3lem7fi  16953  cbvrald  17054  bj-nalset  17159  bj-sels  17178  bj-nnelirr  17217  stnot  17277  isomninnlem  17318  iswomninnlem  17339  iswomni0  17341  ismkvnnlem  17342