Theorem bitr4d 281

Description: Deduction form of bitr4i 277. (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 278	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  306  3bitr2rd  307  3bitr4d  310  3bitr4rd  311  bianabs  540  mpbirand  705  sb3b  2470  sbcom3  2500  sbal1  2522  sbal2  2523  2reu4lem  4530  issn  4839  disjprgw  5148  disjprg  5149  reuhypd  5423  snelpwg  5448  ordtri3  6412  ordsssuc  6465  iota1  6531  funbrfv2b  6960  dffn5  6961  feqmptdf  6973  unima  6977  dmfco  6998  fneqeql  7059  f1ompt  7125  dff13  7270  fliftcnv  7323  soisores  7339  isotr  7348  isoini  7350  caovord3  7639  releldm2  8057  fimaproj  8149  brtpos  8250  tpostpos  8261  oe1m  8575  oawordri  8580  oalimcl  8590  omlimcl  8608  omabs  8681  iserd  8760  qliftel  8829  qliftfun  8831  qliftf  8834  ecopovsym  8848  pw2f1olem  9114  mapen  9179  findcard3  9319  suppeqfsuppbi  9422  mapfien  9451  supisolem  9516  cantnflem1  9732  wemapwe  9740  rankr1clem  9863  rankr1c  9864  ranklim  9887  r1pwALT  9889  r1pwcl  9890  isfin1-2  10428  isfin1-4  10430  fin71num  10440  axdc3lem2  10494  ltmnq  11015  prlem936  11090  ltsosr  11137  ltasr  11143  xrlenlt  11329  ltxrlt  11334  letri3  11349  ne0gt0  11369  subadd  11513  ltsubadd2  11735  lesubadd2  11737  suble  11742  ltsub23  11744  ltaddpos2  11755  ltsubpos  11756  subge02  11780  ltord2  11793  leord2  11794  ltaddsublt  11891  divmul  11926  divmul3  11928  rec11r  11964  ltdiv1  12130  ltdivmul2  12143  ledivmul2  12145  ltrec  12148  ltdiv2  12152  negfi  12215  negiso  12246  nnle1eq1  12294  avgle1  12504  avgle2  12505  avgle  12506  nn0le0eq0  12552  elz2  12628  znnnlt1  12641  zleltp1  12665  difrp  13066  xrltlen  13179  dfle2  13180  xrletri3  13187  xgepnf  13198  xlemnf  13200  qbtwnre  13232  xltnegi  13249  supxrre  13360  infxrre  13369  elioo5  13435  elfz5  13547  elfzm11  13626  predfz  13680  flbi  13836  flbi2  13837  fldiv4lem1div2uz2  13856  fznnfl  13882  zmodid2  13919  2submod  13952  lt2sq  14152  le2sq  14153  sqlecan  14227  bcval5  14335  pfxsuffeqwrdeq  14706  shftfib  15077  mulre  15126  cnpart  15245  01sqrexlem6  15252  sqrmo  15256  elicc4abs  15324  abs2difabs  15339  cau4  15361  limsupgre  15483  clim2  15506  ello1mpt2  15524  lo1resb  15566  o1resb  15568  climeq  15569  climmpt2  15575  isercoll  15672  caucvgb  15684  fsumabs  15805  isumshft  15843  geomulcvg  15880  absefib  16200  dvdsval3  16260  dvdsabseq  16315  dvdsflip  16319  dvdsssfz1  16320  mod2eq1n2dvds  16349  ndvdsadd  16412  bitscmp  16438  smupvallem  16483  dvdssq  16568  lcmdvds  16609  ncoprmgcdgt1b  16652  isprm3  16684  isprm5  16708  phiprmpw  16778  prmdiv  16787  pc11  16882  pcz  16883  pockthlem  16907  prmreclem2  16919  prmreclem4  16921  prmreclem6  16923  1arith  16929  vdwapun  16976  rami  17017  ramcl  17031  pwsle  17507  ercpbllem  17563  invsym  17778  funcres2c  17923  latnle  18498  grpinvcnv  19001  subgacs  19155  eqger  19172  ghmqusker  19281  gexdvds2  19583  pgpfi1  19593  pgpfi  19603  lsmass  19667  lssnle  19672  lsmdisj3b  19688  lsmhash  19703  ablsubadd  19807  gsumval3lem2  19904  subgdmdprd  20034  pgpfac1lem2  20075  dvdsr02  20354  issubrg3  20584  isdomn3  20693  drngid2  20730  sdrgunit  20775  sdrgacs  20780  lssacs  20944  prmirred  21464  chrdvds  21520  chrcong  21521  chrnzr  21524  znleval  21552  znleval2  21553  cygznlem3  21567  frlmbas  21753  elfilspd  21801  lindfmm  21825  islindf4  21836  islindf5  21837  psrbaglefi  21929  psrbaglefiOLD  21930  coe1mul2lem1  22258  mdetunilem9  22613  isneip  23100  neiptopnei  23127  lpdifsn  23138  restopnb  23170  restopn2  23172  restdis  23173  restperf  23179  lmbr2  23254  cncls2  23268  cnprest  23284  cnprest2  23285  iscnrm2  23333  ist0-2  23339  ist1-3  23344  ishaus2  23346  cmpfi  23403  dfconn2  23414  1stccnp  23457  subislly  23476  hausmapdom  23495  tx1cn  23604  tx2cn  23605  txcnmpt  23619  txrest  23626  hauseqlcld  23641  tgqtop  23707  qtopcld  23708  ordthmeolem  23796  trfil2  23882  trfil3  23883  trnei  23887  ufildr  23926  fmfg  23944  rnelfm  23948  fmfnfm  23953  elflim  23966  flimrest  23978  cnflf  23997  cnflf2  23998  ptcmplem2  24048  ghmcnp  24110  tsmssubm  24138  iscfilu  24284  xmetgt0  24355  prdsxmetlem  24365  blcomps  24390  blcom  24391  xblpnfps  24392  xblpnf  24393  blpnf  24394  xmeter  24430  setsxms  24478  imasf1obl  24488  stdbdbl  24517  metrest  24524  metuel2  24565  dscopn  24573  xrtgioo  24813  metdstri  24858  cnmpopc  24940  iihalf2  24946  icopnfhmeo  24959  evth2  24977  lmmbr3  25279  iscau3  25297  metcld  25325  cfilucfil3  25339  srabn  25379  rrxmet  25427  minveclem4  25451  evthicc2  25480  ovolgelb  25500  shft2rab  25528  ovolshftlem1  25529  sca2rab  25532  ovolscalem1  25533  ioombl1lem4  25581  mbfmulc2lem  25667  ismbf3d  25674  mbfsup  25684  mbfinf  25685  i1f1lem  25709  i1fmulclem  25723  mbfi1fseqlem4  25739  itg2seq  25763  ditgneg  25877  limcdif  25896  limcnlp  25898  cnplimc  25907  rolle  26013  mvth  26016  dvne0  26035  lhop1lem  26037  itgsubst  26075  mdegle0  26104  deg1leb  26122  deg1le0  26138  q1peqb  26183  coemulhi  26281  dgrlt  26294  plydivlem3  26323  vieta1lem2  26339  aannenlem1  26356  ulmres  26417  reefiso  26478  pilem3  26483  ellogdm  26666  root1eq1  26783  angpieqvdlem  26856  angpieqvdlem2  26857  quad2  26867  1cubr  26870  quart  26889  rlimcnp  26993  wilthlem2  27097  isppw  27142  dvdsflsumcom  27216  fsumvma  27242  logfac2  27246  chpchtsum  27248  dchrmulcl  27278  dchrresb  27288  bclbnd  27309  bposlem1  27313  bposlem5  27317  gausslemma2dlem0c  27387  lgsquadlem1  27409  m1lgs  27417  2lgsoddprmlem2  27438  dchrisumlem3  27520  dchrisum0lem1  27545  sltval2  27686  noextenddif  27698  sleloe  27784  sletri3  27785  eqscut  27835  elmade2  27892  sltadd1  28006  negsunif  28064  sltsub1  28083  sltsubadd2d  28097  mulsproplem12  28128  sltmul2  28172  sltmul1d  28174  divsmulw  28193  sltdivmul2wd  28200  n0subs  28326  elzn0s  28342  tgjustr  28401  trgcgrg  28442  lnrot1  28550  islnopp  28666  ismidb  28705  islmib  28714  axsegconlem6  28856  axeuclidlem  28896  axcontlem2  28899  axcontlem4  28901  axcontlem12  28909  ausgrusgrb  29101  nb3grpr2  29319  cplgr2v  29368  umgr2v2enb1  29463  crctcsh  29758  clwwlknonwwlknonb  30039  eupth2lems  30171  nmoreltpnf  30702  isblo2  30716  nmlnogt0  30730  phoeqi  30790  ubthlem2  30804  hire  31027  normgt0  31060  ho01i  31761  ho02i  31762  hoeq1  31763  hoeq2  31764  nmopreltpnf  31802  adjeq  31868  leop  32056  leopmul2i  32068  pjnormssi  32101  pjimai  32109  jplem1  32201  mddmd2  32242  mdslmd1lem1  32258  mdslmd1lem2  32259  superpos  32287  atnssm0  32309  dmdbr5ati  32355  disjunsn  32514  fcoinvbr  32525  ofpreima  32582  funcnv5mpt  32585  suppiniseg  32598  isoun  32613  fpwrelmapffslem  32646  fpwrelmap  32647  iocinioc2  32681  xrdifh  32682  nndiffz1  32688  xdivmul  32786  cntzsnid  32930  isarchi2  33050  erler  33120  elrsp  33247  lsmsnpridl  33273  lsmssass  33277  r1pid2OLD  33476  finexttrb  33551  algextdeglem6  33589  algextdeglem7  33590  smatrcl  33611  rhmpreimacnlem  33699  sqsscirc2  33724  xrmulc1cn  33745  esumfsup  33903  1stmbfm  34094  2ndmbfm  34095  mbfmcnt  34102  eulerpartlems  34194  eulerpartlemd  34200  ballotlemfc0  34326  ballotlemfcc  34327  ballotlemsima  34349  ballotlemfrcn0  34363  sgn3da  34375  reprinfz1  34468  reprdifc  34473  bnj1173  34847  zltp1ne  34937  lfuhgr2  34946  erdszelem7  35025  erdszelem9  35027  iscvm  35087  cvmlift3lem4  35150  rexxfr3dALT  35467  fscgr  35904  seglelin  35940  btwnoutside  35949  lineunray  35971  cldbnd  36038  isfne4  36052  fneval  36064  filnetlem4  36093  nndivsub  36169  bj-gabima  36646  dfgcd3  37031  fvineqsneu  37118  wl-sbhbt  37249  wl-sbcom2d  37256  wl-sbalnae  37257  wl-ax11-lem8  37287  sin2h  37311  cos2h  37312  matunitlindflem1  37317  matunitlindflem2  37318  matunitlindf  37319  ptrest  37320  poimirlem3  37324  poimirlem4  37325  poimirlem22  37343  poimirlem27  37348  mblfinlem3  37360  mblfinlem4  37361  ismblfin  37362  itg2addnclem  37372  itg2addnclem2  37373  itg2gt0cn  37376  iblabsnclem  37384  ftc1anclem6  37399  areacirclem2  37410  areacirclem5  37413  areacirc  37414  mettrifi  37458  drngoi  37652  eldm4  37972  exanres2  37995  disjecxrn  38087  brcoss2  38130  br1cossres2  38138  eldmcoss2  38157  eldm1cossres2  38159  brcosscnv2  38171  erimeq2  38376  disjlem19  38499  prter3  38580  islshpat  38715  lsatnle  38742  ellkr2  38789  lshpkr  38815  lkr0f2  38859  lduallkr3  38860  lkreqN  38868  cvrval2  38972  isat3  39005  glbconN  39075  glbconNOLD  39076  hlrelat5N  39100  cvrval4N  39113  atlt  39136  1cvrco  39171  pmaple  39460  isline2  39473  isline4N  39476  elpaddn0  39499  elpadd2at2  39506  cdlemkid4  40633  dia0  40751  cdlemm10N  40817  dibglbN  40865  dihmeetlem4preN  41005  dochkrshp3  41087  dvh4dimlem  41142  lcfl5  41195  mapdpglem3  41374  mapdheq  41427  hdmap1eq  41500  hdmapval2lem  41530  hdmapoc  41630  hlhillcs  41661  lcmineqlem18  41745  fsuppssind  42065  dvdsexpb  42130  renegadd  42152  resubadd  42159  mulgt0b2d  42240  fz1eqin  42426  diophin  42429  jm2.19  42651  rmxdiophlem  42673  pw2f1ocnv  42695  wepwsolem  42703  gicabl  42760  idomodle  42856  onsupmaxb  42904  cantnf2  42991  tfsconcatb0  43010  tfsnfin  43018  ntrclsfveq2  43728  ntrclsss  43730  ntrclsk4  43739  extoimad  43831  radcnvrat  43988  bcc0  44014  supxrre3rnmpt  45044  clim2f  45257  clim2f2  45291  liminfreuzlem  45423  liminfltlem  45425  xlimmnflimsup2  45473  xlimpnfliminf2  45482  xlimlimsupleliminf  45484  opprb  46646  funbrafv2b  46772  dfafn5a  46773  leaddsuble  46910  iccpartgtprec  46992  flsqrt  47165  dfeven2  47221  dfodd3  47222  lindslinindimp2lem4  47844  snlindsntor  47854  regt1loggt0  47924  elbigo2  47940  elbigolo1  47945  fldivexpfllog2  47953  nnlog2ge0lt1  47954  blenpw2m1  47967  naryfvalelwrdf  48021  isprsd  48289  functhinclem1  48362  thincciso  48370  thinciso  48381  prstcprs  48396  postc  48403