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  6515  mpoxopovel  6516  tpostpos  6539  smoiso  6577  frecabcl  6674  frecsuclem  6681  nnaordr  6787  nnaword  6788  nnaordex  6805  ereq1  6818  brdifun  6838  erth2  6858  qliftfun  6895  brecop  6903  elmapg  6939  elpmg  6942  mapsnd  6975  dom2lem  7063  xpcomco  7129  pw2f1odclem  7139  php5fin  7191  funisfsupp  7297  ffsuppbi  7306  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  fcdmnn0fsuppg  9630  znnsub  9708  zgt0ge1  9715  zltlen  9736  nn0n0n1ge2b  9737  nn0le2is012  9740  btwnnz  9752  gtndiv  9753  prime  9757  eluz2  9944  indstr2  10026  negm  10032  nn01to3  10034  qapne  10056  qltlen  10057  qreccl  10059  irrmulap  10066  divlt1lt  10143  divle1le  10144  nnledivrp  10185  xnn0xadd0  10287  xltadd2  10297  xsubge0  10301  xlesubadd  10303  iccid  10345  elioc2  10356  elico2  10357  elicc2  10358  elfz2  10436  fzen  10465  fzsubel  10484  elfzp1  10497  fzpr  10502  fzrevral2  10531  fzrevral3  10532  nn0disj  10563  2ffzeq  10566  fzosplitsni  10672  fvinim0ffz  10678  ioo0  10712  ico0  10714  ioc0  10715  modq0  10788  negqmod0  10790  zmodidfzo  10812  frecuzrdgtcl  10871  nn0ennn  10892  nninfinf  10902  sq11  11071  nn0le2msqd  11180  nn0opth2d  11184  hashen  11246  zfz1isolem1  11315  zfz1iso  11316  csbwrdg  11357  wrdnval  11358  eqwrd  11368  ccat0  11387  ccatws1lenp1bg  11426  swrd0g  11455  swrdspsleq  11462  pfxeq  11491  pfxsuffeqwrdeq  11493  pfxsuff1eqwrdeq  11494  ccatopth2  11512  wrd2ind  11518  2shfti  11619  cjap  11695  cnreim  11767  rexfiuz  11778  rexanuz2  11780  abs00ap  11851  absext  11852  sqabs  11872  abslt  11878  absle  11879  absdiflt  11882  absdifle  11883  lenegsq  11885  minmax  12021  ltmininf  12026  mingeb  12034  xrminmax  12057  xrmin1inf  12059  xrmin2inf  12060  xrltmininf  12062  xrlemininf  12063  clim  12073  clim0c  12078  climrecvg1n  12140  zsumdc  12177  fsum2dlemstep  12227  binomlem  12276  pwm1geoserap1  12301  zproddc  12372  efieq  12528  sin01bnd  12550  cos01bnd  12551  dvdsval2  12583  modm1div  12593  zdvdsdc  12605  modmulconst  12616  dvdsaddr  12630  dvdsabseq  12640  fzocongeq  12651  zeo3  12661  odd2np1  12666  oddp1d2  12683  zob  12684  oddm1d2  12685  nnoddm1d2  12703  divalgb  12718  divalgmod  12720  modremain  12722  bits0  12741  bitsp1e  12745  bitsp1o  12746  bitscmp  12751  bitsinv1lem  12754  gcdn0gt0  12781  bezoutlemstep  12800  dvdssq  12834  nn0seqcvgd  12845  algcvgblem  12853  lcmdvds  12883  lcmgcdeq  12887  coprmdvds  12896  qredeq  12900  congr  12904  isprm2  12921  isprm3  12922  prmdvdsexp  12953  prmdvdsexpb  12954  prmexpb  12956  prmfac1  12957  cncongrprm  12962  nnmaxpwlemxy  12974  nnmaxpwlemnfac  12977  qnumdenbi  12998  qnumgt0  13004  hashdvds  13029  crth  13032  fermltl  13042  modprminveq  13059  pcpremul  13102  pc2dvds  13139  pcz  13141  prmpwdvds  13164  4sqlem16  13215  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemodife  13299  ballotfilemrv1  13323  ballotfilemrv2  13324  ballotfilem1ri  13337  oddennn  13342  ctinfomlemom  13377  mgm1  13750  ismhm  13828  mhmpropd  13833  issubm  13839  issubm2  13840  grpsubrcan  13946  grplactcnv  13967  grp1  13971  eqgval  14086  eqgid  14089  quselbasg  14093  isghm  14106  conjnmzb  14143  iscmn  14187  eqgabl  14225  prdsbasmpt  14288  prdsbasmpt2  14296  rngmneg1  14354  rngmneg2  14355  rngpropd  14362  rngen1zr  14368  srgen1zr0  14400  ringideu  14429  ringpropd  14451  crngpropd  14452  dvdsrd  14511  dvdsr02  14522  opprunitd  14527  crngunit  14528  unitpropdg  14565  rhmunitinv  14595  isnzr2  14601  issubrng  14617  resrhm2b  14667  aprval  14701  aprunit  14702  isdrngtap  14716  opprdrng  14730  islmod  14737  islssm  14804  islssmg  14805  ellspsn  14864  isridl  14951  zrhrhmb  15067  zndvds  15094  znleval  15098  isassa  15112  istopg  15237  eltg  15290  eltg2  15291  tgss2  15317  bastop1  15321  bastop2  15322  iscld  15341  isnei  15382  neiint  15383  iscn  15435  iscnp  15437  iscnp3  15441  tgcn  15446  ssidcn  15448  lmbr2  15452  lmbrf  15453  cnnei  15470  cnrest2  15474  eltx  15497  imasnopn  15537  ispsmet  15561  ismet  15582  isxmet  15583  metn0  15616  xmetres2  15617  elbl3ps  15632  elbl3  15633  xblpnfps  15636  xblpnf  15637  elmopn2  15687  metss  15732  bdxmet  15739  metrest  15744  xmetxp  15745  xmetxpbl  15746  metcnp3  15749  metcnp  15750  metcnp2  15751  metcn  15752  txmetcnp  15756  txmetcn  15757  metcnpd  15758  bl2ioo  15788  addcncntoplem  15799  elcncf  15811  elcncf2  15812  ivthdec  15882  ellimc3apf  15898  cnlimcim  15909  dveflem  15964  ply1termlem  15980  sincosq2sgn  16066  sinq12gt0  16069  logltb  16116  ltexp2  16189  birthdaylem3  16239  wilthlem1  16244  ppiublem1  16303  prmefexple  16320  bposlem1  16323  bposlem6  16328  bposlem7  16329  lgsdilem  16363  lgsdir2lem4  16367  lgsdir2  16369  lgsne0  16374  lgsabs1  16375  gausslemma2dlem3  16399  gausslemma2dlem7  16404  lgseisenlem3  16408  lgsquad3  16420  2lgslem1a  16424  2lgslem3c  16431  2lgslem3d  16432  2lgsoddprmlem4  16448  2sqlem7  16457  2sqlem8a  16458  uhgreq12g  16534  isuhgropm  16539  uhgr0e  16540  upgrop  16562  uhgrvtxedgiedgb  16601  isuspgropen  16622  isusgropen  16623  uhgr2edg  16664  issubgr2  16716  uhgrspansubgrlem  16734  vtxd0nedgbfi  16757  1loopgrvd0fi  16764  iswlk  16781  upgriswlkdc  16818  istrl  16843  iseupth  16905  eupth2lem2dc  16917  eupth2lem3lem3fi  16928  eupth2lem3lem4fi  16931  eupth2lem3lem7fi  16932  cbvrald  17033  bj-nalset  17138  bj-sels  17157  bj-nnelirr  17196  stnot  17256  isomninnlem  17297  iswomninnlem  17318  iswomni0  17320  ismkvnnlem  17321