Theorem bitr4d 282

Description: Deduction form of bitr4i 278. (Contributed by NM, 30-Jun-1993.)

Hypotheses

Ref	Expression
bitr4d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bitr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))

Assertion

Ref	Expression
bitr4d	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem bitr4d

Step	Hyp	Ref	Expression
1		bitr4d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bitr4d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	2	bicomd 222	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 279	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  3bitr2d  307  3bitr2rd  308  3bitr4d  311  3bitr4rd  312  bianabs  541  mpbirand  706  sb3b  2470  sbcom3  2500  sbal1  2522  sbal2  2523  2reu4lem  4521  issn  4829  disjprgw  5137  disjprg  5138  reuhypd  5413  snelpwg  5438  ordtri3  6399  ordsssuc  6452  iota1  6519  funbrfv2b  6950  dffn5  6951  feqmptdf  6963  unima  6967  dmfco  6988  fneqeql  7049  f1ompt  7115  dff13  7259  fliftcnv  7313  soisores  7329  isotr  7338  isoini  7340  caovord3  7628  releldm2  8041  fimaproj  8134  brtpos  8234  tpostpos  8245  oe1m  8559  oawordri  8564  oalimcl  8574  omlimcl  8592  omabs  8665  iserd  8744  qliftel  8810  qliftfun  8812  qliftf  8815  ecopovsym  8829  pw2f1olem  9092  mapen  9157  findcard3  9301  suppeqfsuppbi  9394  mapfien  9423  supisolem  9488  cantnflem1  9704  wemapwe  9712  rankr1clem  9835  rankr1c  9836  ranklim  9859  r1pwALT  9861  r1pwcl  9862  isfin1-2  10400  isfin1-4  10402  fin71num  10412  axdc3lem2  10466  ltmnq  10987  prlem936  11062  ltsosr  11109  ltasr  11115  xrlenlt  11301  ltxrlt  11306  letri3  11321  ne0gt0  11341  subadd  11485  ltsubadd2  11707  lesubadd2  11709  suble  11714  ltsub23  11716  ltaddpos2  11727  ltsubpos  11728  subge02  11752  ltord2  11765  leord2  11766  ltaddsublt  11863  divmul  11897  divmul3  11899  rec11r  11935  ltdiv1  12100  ltdivmul2  12113  ledivmul2  12115  ltrec  12118  ltdiv2  12122  negfi  12185  negiso  12216  nnle1eq1  12264  avgle1  12474  avgle2  12475  avgle  12476  nn0le0eq0  12522  elz2  12598  znnnlt1  12611  zleltp1  12635  difrp  13036  xrltlen  13149  dfle2  13150  xrletri3  13157  xgepnf  13168  xlemnf  13170  qbtwnre  13202  xltnegi  13219  supxrre  13330  infxrre  13339  elioo5  13405  elfz5  13517  elfzm11  13596  predfz  13650  flbi  13805  flbi2  13806  fldiv4lem1div2uz2  13825  fznnfl  13851  zmodid2  13888  2submod  13921  lt2sq  14121  le2sq  14122  sqlecan  14196  bcval5  14301  pfxsuffeqwrdeq  14672  shftfib  15043  mulre  15092  cnpart  15211  01sqrexlem6  15218  sqrmo  15222  elicc4abs  15290  abs2difabs  15305  cau4  15327  limsupgre  15449  clim2  15472  ello1mpt2  15490  lo1resb  15532  o1resb  15534  climeq  15535  climmpt2  15541  isercoll  15638  caucvgb  15650  fsumabs  15771  isumshft  15809  geomulcvg  15846  absefib  16166  dvdsval3  16226  dvdsabseq  16281  dvdsflip  16285  dvdsssfz1  16286  mod2eq1n2dvds  16315  ndvdsadd  16378  bitscmp  16404  smupvallem  16449  dvdssq  16529  lcmdvds  16570  ncoprmgcdgt1b  16613  isprm3  16645  isprm5  16669  phiprmpw  16736  prmdiv  16745  pc11  16840  pcz  16841  pockthlem  16865  prmreclem2  16877  prmreclem4  16879  prmreclem6  16881  1arith  16887  vdwapun  16934  rami  16975  ramcl  16989  pwsle  17465  ercpbllem  17521  invsym  17736  funcres2c  17881  latnle  18456  grpinvcnv  18954  subgacs  19107  eqger  19124  ghmqusker  19229  gexdvds2  19531  pgpfi1  19541  pgpfi  19551  lsmass  19615  lssnle  19620  lsmdisj3b  19636  lsmhash  19651  ablsubadd  19755  gsumval3lem2  19852  subgdmdprd  19982  pgpfac1lem2  20023  dvdsr02  20300  issubrg3  20528  drngid2  20634  sdrgunit  20673  sdrgacs  20678  lssacs  20840  prmirred  21387  chrdvds  21443  chrcong  21444  chrnzr  21447  znleval  21475  znleval2  21476  cygznlem3  21490  frlmbas  21676  elfilspd  21724  lindfmm  21748  islindf4  21759  islindf5  21760  psrbaglefi  21852  psrbaglefiOLD  21853  coe1mul2lem1  22173  mdetunilem9  22509  isneip  22996  neiptopnei  23023  lpdifsn  23034  restopnb  23066  restopn2  23068  restdis  23069  restperf  23075  lmbr2  23150  cncls2  23164  cnprest  23180  cnprest2  23181  iscnrm2  23229  ist0-2  23235  ist1-3  23240  ishaus2  23242  cmpfi  23299  dfconn2  23310  1stccnp  23353  subislly  23372  hausmapdom  23391  tx1cn  23500  tx2cn  23501  txcnmpt  23515  txrest  23522  hauseqlcld  23537  tgqtop  23603  qtopcld  23604  ordthmeolem  23692  trfil2  23778  trfil3  23779  trnei  23783  ufildr  23822  fmfg  23840  rnelfm  23844  fmfnfm  23849  elflim  23862  flimrest  23874  cnflf  23893  cnflf2  23894  ptcmplem2  23944  ghmcnp  24006  tsmssubm  24034  iscfilu  24180  xmetgt0  24251  prdsxmetlem  24261  blcomps  24286  blcom  24287  xblpnfps  24288  xblpnf  24289  blpnf  24290  xmeter  24326  setsxms  24374  imasf1obl  24384  stdbdbl  24413  metrest  24420  metuel2  24461  dscopn  24469  xrtgioo  24709  metdstri  24754  cnmpopc  24836  iihalf2  24842  icopnfhmeo  24855  evth2  24873  lmmbr3  25175  iscau3  25193  metcld  25221  cfilucfil3  25235  srabn  25275  rrxmet  25323  minveclem4  25347  evthicc2  25376  ovolgelb  25396  shft2rab  25424  ovolshftlem1  25425  sca2rab  25428  ovolscalem1  25429  ioombl1lem4  25477  mbfmulc2lem  25563  ismbf3d  25570  mbfsup  25580  mbfinf  25581  i1f1lem  25605  i1fmulclem  25619  mbfi1fseqlem4  25635  itg2seq  25659  ditgneg  25773  limcdif  25792  limcnlp  25794  cnplimc  25803  rolle  25909  mvth  25912  dvne0  25931  lhop1lem  25933  itgsubst  25971  mdegle0  26000  deg1leb  26018  deg1le0  26034  q1peqb  26078  coemulhi  26175  dgrlt  26188  plydivlem3  26217  vieta1lem2  26233  aannenlem1  26250  ulmres  26311  reefiso  26372  pilem3  26377  ellogdm  26560  root1eq1  26677  angpieqvdlem  26747  angpieqvdlem2  26748  quad2  26758  1cubr  26761  quart  26780  rlimcnp  26884  wilthlem2  26988  isppw  27033  dvdsflsumcom  27107  fsumvma  27133  logfac2  27137  chpchtsum  27139  dchrmulcl  27169  dchrresb  27179  bclbnd  27200  bposlem1  27204  bposlem5  27208  gausslemma2dlem0c  27278  lgsquadlem1  27300  m1lgs  27308  2lgsoddprmlem2  27329  dchrisumlem3  27411  dchrisum0lem1  27436  sltval2  27576  noextenddif  27588  sleloe  27674  sletri3  27675  eqscut  27725  elmade2  27782  sltadd1  27896  negsunif  27954  sltsub1  27971  sltsubadd2d  27985  mulsproplem12  28014  sltmul2  28058  sltmul1d  28060  divsmulw  28079  sltdivmul2wd  28086  tgjustr  28265  trgcgrg  28306  lnrot1  28414  islnopp  28530  ismidb  28569  islmib  28578  axsegconlem6  28720  axeuclidlem  28760  axcontlem2  28763  axcontlem4  28765  axcontlem12  28773  ausgrusgrb  28965  nb3grpr2  29183  cplgr2v  29232  umgr2v2enb1  29327  crctcsh  29622  clwwlknonwwlknonb  29903  eupth2lems  30035  nmoreltpnf  30566  isblo2  30580  nmlnogt0  30594  phoeqi  30654  ubthlem2  30668  hire  30891  normgt0  30924  ho01i  31625  ho02i  31626  hoeq1  31627  hoeq2  31628  nmopreltpnf  31666  adjeq  31732  leop  31920  leopmul2i  31932  pjnormssi  31965  pjimai  31973  jplem1  32065  mddmd2  32106  mdslmd1lem1  32122  mdslmd1lem2  32123  superpos  32151  atnssm0  32173  dmdbr5ati  32219  disjunsn  32369  fcoinvbr  32380  ofpreima  32434  funcnv5mpt  32437  suppiniseg  32450  isoun  32465  fpwrelmapffslem  32498  fpwrelmap  32499  iocinioc2  32531  xrdifh  32532  nndiffz1  32538  xdivmul  32630  cntzsnid  32753  isarchi2  32871  elrsp  33025  lsmsnpridl  33047  lsmssass  33051  r1pid2  33211  finexttrb  33286  algextdeglem6  33326  algextdeglem7  33327  smatrcl  33333  rhmpreimacnlem  33421  sqsscirc2  33446  xrmulc1cn  33467  esumfsup  33625  1stmbfm  33816  2ndmbfm  33817  mbfmcnt  33824  eulerpartlems  33916  eulerpartlemd  33922  ballotlemfc0  34048  ballotlemfcc  34049  ballotlemsima  34071  ballotlemfrcn0  34085  sgn3da  34097  reprinfz1  34190  reprdifc  34195  bnj1173  34569  zltp1ne  34655  lfuhgr2  34664  erdszelem7  34743  erdszelem9  34745  iscvm  34805  cvmlift3lem4  34868  fscgr  35612  seglelin  35648  btwnoutside  35657  lineunray  35679  cldbnd  35746  isfne4  35760  fneval  35772  filnetlem4  35801  nndivsub  35877  bj-gabima  36354  dfgcd3  36739  fvineqsneu  36826  wl-sbhbt  36956  wl-sbcom2d  36963  wl-sbalnae  36964  wl-ax11-lem8  36994  sin2h  37018  cos2h  37019  matunitlindflem1  37024  matunitlindflem2  37025  matunitlindf  37026  ptrest  37027  poimirlem3  37031  poimirlem4  37032  poimirlem22  37050  poimirlem27  37055  mblfinlem3  37067  mblfinlem4  37068  ismblfin  37069  itg2addnclem  37079  itg2addnclem2  37080  itg2gt0cn  37083  iblabsnclem  37091  ftc1anclem6  37106  areacirclem2  37117  areacirclem5  37120  areacirc  37121  mettrifi  37165  drngoi  37359  eldm4  37681  exanres2  37705  disjecxrn  37798  brcoss2  37841  br1cossres2  37849  eldmcoss2  37868  eldm1cossres2  37870  brcosscnv2  37882  erimeq2  38087  disjlem19  38210  prter3  38291  islshpat  38426  lsatnle  38453  ellkr2  38500  lshpkr  38526  lkr0f2  38570  lduallkr3  38571  lkreqN  38579  cvrval2  38683  isat3  38716  glbconN  38786  glbconNOLD  38787  hlrelat5N  38811  cvrval4N  38824  atlt  38847  1cvrco  38882  pmaple  39171  isline2  39184  isline4N  39187  elpaddn0  39210  elpadd2at2  39217  cdlemkid4  40344  dia0  40462  cdlemm10N  40528  dibglbN  40576  dihmeetlem4preN  40716  dochkrshp3  40798  dvh4dimlem  40853  lcfl5  40906  mapdpglem3  41085  mapdheq  41138  hdmap1eq  41211  hdmapval2lem  41241  hdmapoc  41341  hlhillcs  41372  lcmineqlem18  41454  fsuppssind  41748  dvdsexpb  41824  renegadd  41849  resubadd  41856  mulgt0b2d  41937  fz1eqin  42111  diophin  42114  jm2.19  42336  rmxdiophlem  42358  pw2f1ocnv  42380  wepwsolem  42388  gicabl  42445  idomodle  42541  isdomn3  42549  onsupmaxb  42590  cantnf2  42677  tfsconcatb0  42696  tfsnfin  42704  ntrclsfveq2  43414  ntrclsss  43416  ntrclsk4  43425  extoimad  43517  radcnvrat  43674  bcc0  43700  supxrre3rnmpt  44734  clim2f  44947  clim2f2  44981  liminfreuzlem  45113  liminfltlem  45115  xlimmnflimsup2  45163  xlimpnfliminf2  45172  xlimlimsupleliminf  45174  opprb  46336  funbrafv2b  46462  dfafn5a  46463  leaddsuble  46600  iccpartgtprec  46683  flsqrt  46856  dfeven2  46912  dfodd3  46913  lindslinindimp2lem4  47452  snlindsntor  47462  regt1loggt0  47532  elbigo2  47548  elbigolo1  47553  fldivexpfllog2  47561  nnlog2ge0lt1  47562  blenpw2m1  47575  naryfvalelwrdf  47629  isprsd  47897  functhinclem1  47970  thincciso  47978  thinciso  47989  prstcprs  48004  postc  48011