Theorem bitr4d 285

Description: Deduction form of bitr4i 281. (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 226	. 2 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
4	1, 3	bitrd 282	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitr2d  310  3bitr2rd  311  3bitr4d  314  3bitr4rd  315  bianabs  551  mpbirand  720  sb3b  2505  sbcom3  2535  sbal1  2557  sbal2  2558  2reu4lem  4478  issn  4791  disjprg  5098  reuhypd  5380  snelpwg  5410  ordtri3  6399  ordsssuc  6454  iota1  6517  funbrfv2b  6942  dffn5  6943  feqmptdf  6955  unima  6960  dmfco  6981  fneqeql  7045  f1ompt  7111  dff13  7258  fliftcnv  7319  soisores  7335  isotr  7344  isoini  7346  caovord3  7634  releldm2  8054  fimaproj  8152  brtpos  8252  tpostpos  8263  oe1m  8553  oawordri  8558  oalimcl  8568  omlimcl  8586  omabs  8660  iserd  8744  qliftel  8821  qliftfun  8823  qliftf  8826  ecopovsym  8840  pw2f1olem  9100  mapen  9160  findcard3  9274  tfsnfin2  9352  suppeqfsuppbi  9371  mapfien  9400  supisolem  9466  cantnflem1  9690  wemapwe  9698  rankr1clem  9829  rankr1c  9830  ranklim  9858  r1pwALT  9860  r1pwcl  9861  isfin1-2  10463  isfin1-4  10465  fin71num  10475  axdc3lem2  10529  infinfg  10650  ltmnq  11057  prlem936  11132  ltsosr  11179  ltasr  11185  xrlenlt  11374  ltxrlt  11380  letri3  11395  ne0gt0  11415  subadd  11560  ltsubadd2  11787  lesubadd2  11789  suble  11794  ltsub23  11796  ltaddpos2  11807  ltsubpos  11808  subge02  11832  ltord2  11845  leord2  11846  ltaddsublt  11943  divmul  11977  divmul3  11979  rec11r  12016  ltdiv1  12181  ltdivmul2  12194  ledivmul2  12196  ltrec  12199  ltdiv2  12203  negfi  12266  negiso  12297  nnle1eq1  12368  avgle1  12586  avgle2  12587  avgle  12588  nn0le0eq0  12634  elz2  12711  znnnlt1  12723  zleltp1  12747  difrp  13160  xrltlen  13275  dfle2  13276  xrletri3  13283  xgepnf  13295  xlemnf  13297  qbtwnre  13329  xltnegi  13346  supxrre  13457  infxrre  13467  elioo5  13534  elfz5  13648  elfzm11  13729  predfz  13787  flbi  13956  flbi2  13957  fldiv4lem1div2uz2  13976  fznnfl  14002  zmodid2  14039  2submod  14075  lt2sq  14276  le2sq  14277  sqlecan  14353  bcval5  14462  pfxsuffeqwrdeq  14847  shftfib  15225  sgn3da  15254  mulre  15288  cnpart  15407  01sqrexlem6  15414  sqrmo  15418  elicc4abs  15487  abs2difabs  15502  cau4  15524  limsupgre  15648  clim2  15671  ello1mpt2  15689  lo1resb  15731  o1resb  15733  climeq  15734  climmpt2  15740  isercoll  15835  caucvgb  15847  fsumabs  15968  isumshft  16008  geomulcvg  16045  absefib  16366  dvdsval3  16426  addmulmodb  16435  dvdsabseq  16483  dvdsflip  16487  dvdsssfz1  16488  mod2eq1n2dvds  16517  ndvdsadd  16580  bitscmp  16608  smupvallem  16653  dvdssq  16742  lcmdvds  16783  ncoprmgcdgt1b  16826  isprm3  16858  isprm5  16883  phiprmpw  16953  prmdiv  16962  pc11  17058  pcz  17059  pockthlem  17083  prmreclem2  17095  prmreclem4  17097  prmreclem6  17099  1arith  17105  vdwapun  17152  rami  17193  ramcl  17207  pwsle  17664  ercpbllem  17720  invsym  17937  funcres2c  18078  latnle  18647  grpinvcnv  19217  subgacs  19371  eqger  19390  ghmqusker  19501  gexdvds2  19799  pgpfi1  19809  pgpfi  19819  lsmass  19883  lssnle  19888  lsmdisj3b  19904  lsmhash  19919  ablsubadd  20023  gsumval3lem2  20120  subgdmdprd  20250  pgpfac1lem2  20291  dvdsr02  20602  issubrg3  20852  isdomn3  20966  drngid2  21010  sdrgunit  21053  sdrgacs  21058  lssacs  21242  prmirred  21780  chrdvds  21832  chrcong  21833  chrnzr  21836  znleval  21860  znleval2  21861  cygznlem3  21875  frlmbas  22061  elfilspd  22109  lindfmm  22133  islindf4  22144  islindf5  22145  psrbaglefi  22234  coe1mul2lem1  22586  mdetunilem9  22935  matunitlindflem1  22994  matunitlindflem2  22995  matunitlindf  22996  isneip  23423  neiptopnei  23450  lpdifsn  23461  restopnb  23493  restopn2  23495  restdis  23496  restperf  23502  lmbr2  23577  cncls2  23591  cnprest  23607  cnprest2  23608  iscnrm2  23656  ist0-2  23662  ist1-3  23667  ishaus2  23669  cmpfi  23726  dfconn2  23737  1stccnp  23781  subislly  23800  hausmapdom  23819  tx1cn  23928  tx2cn  23929  txcnmpt  23943  txrest  23950  hauseqlcld  23965  tgqtop  24031  qtopcld  24032  ordthmeolem  24120  trfil2  24206  trfil3  24207  trnei  24211  ufildr  24250  fmfg  24268  rnelfm  24272  fmfnfm  24277  elflim  24290  flimrest  24302  cnflf  24321  cnflf2  24322  ptcmplem2  24372  ghmcnp  24434  tsmssubm  24462  iscfilu  24606  xmetgt0  24677  prdsxmetlem  24687  blcomps  24712  blcom  24713  xblpnfps  24714  xblpnf  24715  blpnf  24716  xmeter  24752  setsxms  24798  imasf1obl  24807  stdbdbl  24836  metrest  24843  metuel2  24884  dscopn  24892  xrtgioo  25126  metdstri  25171  cnmpopc  25249  iihalf2  25254  icopnfhmeo  25264  evth2  25281  lmmbr3  25581  iscau3  25599  metcld  25627  cfilucfil3  25641  srabn  25681  rrxmet  25729  minveclem4  25753  evthicc2  25781  ovolgelb  25801  shft2rab  25829  ovolshftlem1  25830  sca2rab  25833  ovolscalem1  25834  ioombl1lem4  25882  mbfmulc2lem  25968  ismbf3d  25975  mbfsup  25985  mbfinf  25986  i1f1lem  26010  i1fmulclem  26023  mbfi1fseqlem4  26039  itg2seq  26063  ditgneg  26177  limcdif  26196  limcnlp  26198  cnplimc  26207  rolle  26310  mvth  26312  dvne0  26331  lhop1lem  26333  itgsubst  26369  mdegle0  26395  deg1leb  26413  deg1le0  26429  q1peqb  26474  coemulhi  26573  dgrlt  26585  plydivlem3  26616  vieta1lem2  26634  aannenlem1  26655  ulmres  26715  reefiso  26775  pilem3  26780  ellogdm  26967  root1eq1  27083  angpieqvdlem  27156  angpieqvdlem2  27157  quad2  27167  1cubr  27170  quart  27189  rlimcnp  27293  wilthlem2  27396  isppw  27441  dvdsflsumcom  27515  fsumvma  27540  logfac2  27544  chpchtsum  27546  dchrmulcl  27576  dchrresb  27586  bclbnd  27607  bposlem1  27611  bposlem5  27615  gausslemma2dlem0c  27685  lgsquadlem1  27707  m1lgs  27715  2lgsoddprmlem2  27736  dchrisumlem3  27818  dchrisum0lem1  27843  ltsval2  28013  noextenddif  28025  lesloe  28111  lestri3  28112  eqcuts  28171  elmade2  28244  ltadds1  28378  negsunif  28441  ltsubs1  28462  ltsubadds2d  28476  mulsproplem12  28513  ltmuls2  28557  ltmuls1d  28559  divmulsw  28579  ltdivmuls2wd  28586  oniso  28657  n0subs  28749  n0lesltp1  28752  elzn0s  28784  avglts1d  28839  avglts2d  28840  bdaypw2n0bndlem  28849  z12sge0  28869  dfz12s2  28874  elreno2  28881  tgjustr  28936  trgcgrg  28978  lnrot1  29091  islnopp  29215  elplng  29258  plngcplem  29263  ismidb  29283  islmib  29292  axsegconlem6  29500  axeuclidlem  29540  axcontlem2  29543  axcontlem4  29545  axcontlem12  29553  lfuhgr2  29727  ausgrusgrb  29746  nb3grpr2  29964  cplgr2v  30013  umgr2v2enb1  30107  crctcsh  30413  clwwlknonwwlknonb  30697  eupth2lems  30839  nmoreltpnf  31371  isblo2  31385  nmlnogt0  31399  phoeqi  31459  ubthlem2  31473  hire  31696  normgt0  31729  ho01i  32430  ho02i  32431  hoeq1  32432  hoeq2  32433  nmopreltpnf  32471  adjeq  32537  leop  32725  leopmul2i  32737  pjnormssi  32770  pjimai  32778  jplem1  32870  mddmd2  32911  mdslmd1lem1  32927  mdslmd1lem2  32928  superpos  32956  atnssm0  32978  dmdbr5ati  33024  disjunsn  33230  fcoinvbr  33241  ofpreima  33301  funcnv5mpt  33303  suppiniseg  33321  isoun  33337  fpwrelmapffslem  33366  fpwrelmap  33367  iocinioc2  33413  xrdifh  33414  nndiffz1  33420  xdivmul  33533  cntzsnid  33683  cntrval2  33774  isarchi2  33788  isunitc  33844  erler  33868  rlocisunit  33879  elrsp  33969  lsmsnpridl  33993  lsmssass  33995  esplyind  34249  finexttrb  34339  algextdeglem6  34396  algextdeglem7  34397  smatrcl  34470  rhmpreimacnlem  34558  sqsscirc2  34583  xrmulc1cn  34604  esumfsup  34744  1stmbfm  34934  2ndmbfm  34935  mbfmcnt  34942  eulerpartlems  35034  eulerpartlemd  35040  ballotlemfc0  35167  ballotlemfcc  35168  ballotlemsima  35190  ballotlemfrcn0  35204  reprinfz1  35293  reprdifc  35298  bnj1173  35674  fineqvnttrclse  35834  kardcard2  35876  vonf1wev  35929  vonf1owevOLD  35931  zltp1ne  35942  erdszelem7  36004  erdszelem9  36006  iscvm  36066  cvmlift3lem4  36129  rexxfr3dALT  36446  fscgr  36887  seglelin  36923  btwnoutside  36932  lineunray  36954  cldbnd  37156  isfne4  37170  fneval  37182  filnetlem4  37211  nndivsub  37287  bj-gabima  37895  dfgcd3  38288  fvineqsneu  38377  wl-sbhbt  38529  wl-sbcom2d  38536  wl-sbalnae  38537  sin2h  38576  cos2h  38577  ptrest  38580  poimirlem3  38584  poimirlem4  38585  poimirlem22  38603  poimirlem27  38608  mblfinlem3  38620  mblfinlem4  38621  ismblfin  38622  itg2addnclem  38632  itg2addnclem2  38633  itg2gt0cn  38636  iblabsnclem  38644  ftc1anclem6  38659  areacirclem2  38670  areacirclem5  38673  areacirc  38674  mettrifi  38734  drngoi  38928  eldm4  39256  exanres2  39278  disjecxrn  39387  exeupre  39466  brcoss2  39497  br1cossres2  39505  eldmcoss2  39524  eldm1cossres2  39526  brcosscnv2  39538  erimeq2  39738  disjqmap  39802  disjlem19  39879  prter3  39982  islshpat  40117  lsatnle  40144  ellkr2  40191  lshpkr  40217  lkr0f2  40261  lduallkr3  40262  lkreqN  40270  cvrval2  40374  isat3  40407  glbconN  40477  hlrelat5N  40501  cvrval4N  40514  atlt  40537  1cvrco  40572  pmaple  40861  isline2  40874  isline4N  40877  elpaddn0  40900  elpadd2at2  40907  cdlemkid4  42034  dia0  42152  cdlemm10N  42218  dibglbN  42266  dihmeetlem4preN  42406  dochkrshp3  42488  dvh4dimlem  42543  lcfl5  42596  mapdpglem3  42775  mapdheq  42828  hdmap1eq  42901  hdmapval2lem  42931  hdmapoc  43031  hlhillcs  43058  lcmineqlem18  43139  dvdsexpb  43430  renegadd  43466  resubadd  43473  redivmuld  43539  mulgt0b1d  43579  fsuppssind  43664  frlmnzcoordsca  43701  fz1eqin  43823  diophin  43826  jm2.19  44043  rmxdiophlem  44065  pw2f1ocnv  44087  wepwsolem  44092  gicabl  44144  idomodle  44236  onsupmaxb  44284  cantnf2  44370  tfsconcatb0  44389  tfsnfin  44397  ntrclsfveq2  45104  ntrclsss  45106  ntrclsk4  45115  extoimad  45207  radcnvrat  45341  bcc0  45367  hashomiso  46058  supxrre3rnmpt  46482  clim2f  46689  clim2f2  46723  liminfreuzlem  46855  liminfltlem  46857  xlimmnflimsup2  46905  xlimpnfliminf2  46914  xlimlimsupleliminf  46916  opprb  48144  funbrafv2b  48272  dfafn5a  48273  leaddsuble  48410  mod2addne  48483  iccpartgtprec  48545  flsqrt  48721  dfeven2  48790  dfodd3  48791  lindslinindimp2lem4  49616  snlindsntor  49626  regt1loggt0  49691  elbigo2  49707  elbigolo1  49712  fldivexpfllog2  49720  nnlog2ge0lt1  49721  blenpw2m1  49734  naryfvalelwrdf  49788  isprsd  50106  resccatlem  50224  functhinclem1  50595  thincciso  50604  thinciso  50621  isinito2lem  50649  fulltermc  50662  prstcprs  50711  oduoppcciso  50717  postc  50720  lmdran  50822  cmdlan  50823