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 223	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 279	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3bitr2d  307  3bitr2rd  308  3bitr4d  311  3bitr4rd  312  bianabs  541  mpbirand  706  sb3b  2484  sbcom3  2514  sbal1  2536  sbal2  2537  2reu4lem  4545  issn  4857  disjprg  5162  reuhypd  5437  snelpwg  5462  ordtri3  6431  ordsssuc  6484  iota1  6550  funbrfv2b  6979  dffn5  6980  feqmptdf  6992  unima  6997  dmfco  7018  fneqeql  7079  f1ompt  7145  dff13  7292  fliftcnv  7347  soisores  7363  isotr  7372  isoini  7374  caovord3  7663  releldm2  8084  fimaproj  8176  brtpos  8276  tpostpos  8287  oe1m  8601  oawordri  8606  oalimcl  8616  omlimcl  8634  omabs  8707  iserd  8789  qliftel  8858  qliftfun  8860  qliftf  8863  ecopovsym  8877  pw2f1olem  9142  mapen  9207  findcard3  9346  suppeqfsuppbi  9448  mapfien  9477  supisolem  9542  cantnflem1  9758  wemapwe  9766  rankr1clem  9889  rankr1c  9890  ranklim  9913  r1pwALT  9915  r1pwcl  9916  isfin1-2  10454  isfin1-4  10456  fin71num  10466  axdc3lem2  10520  ltmnq  11041  prlem936  11116  ltsosr  11163  ltasr  11169  xrlenlt  11355  ltxrlt  11360  letri3  11375  ne0gt0  11395  subadd  11539  ltsubadd2  11761  lesubadd2  11763  suble  11768  ltsub23  11770  ltaddpos2  11781  ltsubpos  11782  subge02  11806  ltord2  11819  leord2  11820  ltaddsublt  11917  divmul  11952  divmul3  11954  rec11r  11993  ltdiv1  12159  ltdivmul2  12172  ledivmul2  12174  ltrec  12177  ltdiv2  12181  negfi  12244  negiso  12275  nnle1eq1  12323  avgle1  12533  avgle2  12534  avgle  12535  nn0le0eq0  12581  elz2  12657  znnnlt1  12670  zleltp1  12694  difrp  13095  xrltlen  13208  dfle2  13209  xrletri3  13216  xgepnf  13227  xlemnf  13229  qbtwnre  13261  xltnegi  13278  supxrre  13389  infxrre  13398  elioo5  13464  elfz5  13576  elfzm11  13655  predfz  13710  flbi  13867  flbi2  13868  fldiv4lem1div2uz2  13887  fznnfl  13913  zmodid2  13950  2submod  13983  lt2sq  14183  le2sq  14184  sqlecan  14258  bcval5  14367  pfxsuffeqwrdeq  14746  shftfib  15121  mulre  15170  cnpart  15289  01sqrexlem6  15296  sqrmo  15300  elicc4abs  15368  abs2difabs  15383  cau4  15405  limsupgre  15527  clim2  15550  ello1mpt2  15568  lo1resb  15610  o1resb  15612  climeq  15613  climmpt2  15619  isercoll  15716  caucvgb  15728  fsumabs  15849  isumshft  15887  geomulcvg  15924  absefib  16246  dvdsval3  16306  dvdsabseq  16361  dvdsflip  16365  dvdsssfz1  16366  mod2eq1n2dvds  16395  ndvdsadd  16458  bitscmp  16484  smupvallem  16529  dvdssq  16614  lcmdvds  16655  ncoprmgcdgt1b  16698  isprm3  16730  isprm5  16754  phiprmpw  16823  prmdiv  16832  pc11  16927  pcz  16928  pockthlem  16952  prmreclem2  16964  prmreclem4  16966  prmreclem6  16968  1arith  16974  vdwapun  17021  rami  17062  ramcl  17076  pwsle  17552  ercpbllem  17608  invsym  17823  funcres2c  17968  latnle  18543  grpinvcnv  19046  subgacs  19201  eqger  19218  ghmqusker  19327  gexdvds2  19627  pgpfi1  19637  pgpfi  19647  lsmass  19711  lssnle  19716  lsmdisj3b  19732  lsmhash  19747  ablsubadd  19851  gsumval3lem2  19948  subgdmdprd  20078  pgpfac1lem2  20119  dvdsr02  20398  issubrg3  20628  isdomn3  20737  drngid2  20774  sdrgunit  20819  sdrgacs  20824  lssacs  20988  prmirred  21508  chrdvds  21564  chrcong  21565  chrnzr  21568  znleval  21596  znleval2  21597  cygznlem3  21611  frlmbas  21798  elfilspd  21846  lindfmm  21870  islindf4  21881  islindf5  21882  psrbaglefi  21969  coe1mul2lem1  22291  mdetunilem9  22647  isneip  23134  neiptopnei  23161  lpdifsn  23172  restopnb  23204  restopn2  23206  restdis  23207  restperf  23213  lmbr2  23288  cncls2  23302  cnprest  23318  cnprest2  23319  iscnrm2  23367  ist0-2  23373  ist1-3  23378  ishaus2  23380  cmpfi  23437  dfconn2  23448  1stccnp  23491  subislly  23510  hausmapdom  23529  tx1cn  23638  tx2cn  23639  txcnmpt  23653  txrest  23660  hauseqlcld  23675  tgqtop  23741  qtopcld  23742  ordthmeolem  23830  trfil2  23916  trfil3  23917  trnei  23921  ufildr  23960  fmfg  23978  rnelfm  23982  fmfnfm  23987  elflim  24000  flimrest  24012  cnflf  24031  cnflf2  24032  ptcmplem2  24082  ghmcnp  24144  tsmssubm  24172  iscfilu  24318  xmetgt0  24389  prdsxmetlem  24399  blcomps  24424  blcom  24425  xblpnfps  24426  xblpnf  24427  blpnf  24428  xmeter  24464  setsxms  24512  imasf1obl  24522  stdbdbl  24551  metrest  24558  metuel2  24599  dscopn  24607  xrtgioo  24847  metdstri  24892  cnmpopc  24974  iihalf2  24980  icopnfhmeo  24993  evth2  25011  lmmbr3  25313  iscau3  25331  metcld  25359  cfilucfil3  25373  srabn  25413  rrxmet  25461  minveclem4  25485  evthicc2  25514  ovolgelb  25534  shft2rab  25562  ovolshftlem1  25563  sca2rab  25566  ovolscalem1  25567  ioombl1lem4  25615  mbfmulc2lem  25701  ismbf3d  25708  mbfsup  25718  mbfinf  25719  i1f1lem  25743  i1fmulclem  25757  mbfi1fseqlem4  25773  itg2seq  25797  ditgneg  25912  limcdif  25931  limcnlp  25933  cnplimc  25942  rolle  26048  mvth  26051  dvne0  26070  lhop1lem  26072  itgsubst  26110  mdegle0  26136  deg1leb  26154  deg1le0  26170  q1peqb  26215  coemulhi  26313  dgrlt  26326  plydivlem3  26355  vieta1lem2  26371  aannenlem1  26388  ulmres  26449  reefiso  26510  pilem3  26515  ellogdm  26699  root1eq1  26816  angpieqvdlem  26889  angpieqvdlem2  26890  quad2  26900  1cubr  26903  quart  26922  rlimcnp  27026  wilthlem2  27130  isppw  27175  dvdsflsumcom  27249  fsumvma  27275  logfac2  27279  chpchtsum  27281  dchrmulcl  27311  dchrresb  27321  bclbnd  27342  bposlem1  27346  bposlem5  27350  gausslemma2dlem0c  27420  lgsquadlem1  27442  m1lgs  27450  2lgsoddprmlem2  27471  dchrisumlem3  27553  dchrisum0lem1  27578  sltval2  27719  noextenddif  27731  sleloe  27817  sletri3  27818  eqscut  27868  elmade2  27925  sltadd1  28043  negsunif  28105  sltsub1  28124  sltsubadd2d  28138  mulsproplem12  28171  sltmul2  28215  sltmul1d  28217  divsmulw  28236  sltdivmul2wd  28243  n0subs  28378  elzn0s  28402  tgjustr  28500  trgcgrg  28541  lnrot1  28649  islnopp  28765  ismidb  28804  islmib  28813  axsegconlem6  28955  axeuclidlem  28995  axcontlem2  28998  axcontlem4  29000  axcontlem12  29008  ausgrusgrb  29200  nb3grpr2  29418  cplgr2v  29467  umgr2v2enb1  29562  crctcsh  29857  clwwlknonwwlknonb  30138  eupth2lems  30270  nmoreltpnf  30801  isblo2  30815  nmlnogt0  30829  phoeqi  30889  ubthlem2  30903  hire  31126  normgt0  31159  ho01i  31860  ho02i  31861  hoeq1  31862  hoeq2  31863  nmopreltpnf  31901  adjeq  31967  leop  32155  leopmul2i  32167  pjnormssi  32200  pjimai  32208  jplem1  32300  mddmd2  32341  mdslmd1lem1  32357  mdslmd1lem2  32358  superpos  32386  atnssm0  32408  dmdbr5ati  32454  disjunsn  32616  fcoinvbr  32627  ofpreima  32683  funcnv5mpt  32686  suppiniseg  32698  isoun  32713  fpwrelmapffslem  32746  fpwrelmap  32747  iocinioc2  32784  xrdifh  32785  nndiffz1  32791  xdivmul  32889  cntzsnid  33045  isarchi2  33165  erler  33237  elrsp  33365  lsmsnpridl  33391  lsmssass  33395  r1pid2OLD  33594  finexttrb  33675  algextdeglem6  33713  algextdeglem7  33714  smatrcl  33742  rhmpreimacnlem  33830  sqsscirc2  33855  xrmulc1cn  33876  esumfsup  34034  1stmbfm  34225  2ndmbfm  34226  mbfmcnt  34233  eulerpartlems  34325  eulerpartlemd  34331  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemsima  34480  ballotlemfrcn0  34494  sgn3da  34506  reprinfz1  34599  reprdifc  34604  bnj1173  34978  zltp1ne  35077  lfuhgr2  35086  erdszelem7  35165  erdszelem9  35167  iscvm  35227  cvmlift3lem4  35290  rexxfr3dALT  35607  fscgr  36044  seglelin  36080  btwnoutside  36089  lineunray  36111  cldbnd  36292  isfne4  36306  fneval  36318  filnetlem4  36347  nndivsub  36423  bj-gabima  36906  dfgcd3  37290  fvineqsneu  37377  wl-sbhbt  37508  wl-sbcom2d  37515  wl-sbalnae  37516  wl-ax11-lem8  37546  sin2h  37570  cos2h  37571  matunitlindflem1  37576  matunitlindflem2  37577  matunitlindf  37578  ptrest  37579  poimirlem3  37583  poimirlem4  37584  poimirlem22  37602  poimirlem27  37607  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  itg2addnclem  37631  itg2addnclem2  37632  itg2gt0cn  37635  iblabsnclem  37643  ftc1anclem6  37658  areacirclem2  37669  areacirclem5  37672  areacirc  37673  mettrifi  37717  drngoi  37911  eldm4  38230  exanres2  38253  disjecxrn  38345  brcoss2  38388  br1cossres2  38396  eldmcoss2  38415  eldm1cossres2  38417  brcosscnv2  38429  erimeq2  38634  disjlem19  38757  prter3  38838  islshpat  38973  lsatnle  39000  ellkr2  39047  lshpkr  39073  lkr0f2  39117  lduallkr3  39118  lkreqN  39126  cvrval2  39230  isat3  39263  glbconN  39333  glbconNOLD  39334  hlrelat5N  39358  cvrval4N  39371  atlt  39394  1cvrco  39429  pmaple  39718  isline2  39731  isline4N  39734  elpaddn0  39757  elpadd2at2  39764  cdlemkid4  40891  dia0  41009  cdlemm10N  41075  dibglbN  41123  dihmeetlem4preN  41263  dochkrshp3  41345  dvh4dimlem  41400  lcfl5  41453  mapdpglem3  41632  mapdheq  41685  hdmap1eq  41758  hdmapval2lem  41788  hdmapoc  41888  hlhillcs  41919  lcmineqlem18  42003  dvdsexpb  42322  renegadd  42348  resubadd  42355  mulgt0b2d  42436  fsuppssind  42548  fz1eqin  42725  diophin  42728  jm2.19  42950  rmxdiophlem  42972  pw2f1ocnv  42994  wepwsolem  42999  gicabl  43056  idomodle  43152  onsupmaxb  43200  cantnf2  43287  tfsconcatb0  43306  tfsnfin  43314  ntrclsfveq2  44023  ntrclsss  44025  ntrclsk4  44034  extoimad  44126  radcnvrat  44283  bcc0  44309  supxrre3rnmpt  45344  clim2f  45557  clim2f2  45591  liminfreuzlem  45723  liminfltlem  45725  xlimmnflimsup2  45773  xlimpnfliminf2  45782  xlimlimsupleliminf  45784  opprb  46946  funbrafv2b  47074  dfafn5a  47075  leaddsuble  47212  iccpartgtprec  47294  flsqrt  47467  dfeven2  47523  dfodd3  47524  lindslinindimp2lem4  48190  snlindsntor  48200  regt1loggt0  48270  elbigo2  48286  elbigolo1  48291  fldivexpfllog2  48299  nnlog2ge0lt1  48300  blenpw2m1  48313  naryfvalelwrdf  48367  isprsd  48635  functhinclem1  48708  thincciso  48716  thinciso  48727  prstcprs  48742  postc  48749