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  708  sb3b  2481  sbcom3  2511  sbal1  2533  sbal2  2534  2reu4lem  4464  issn  4776  disjprg  5082  reuhypd  5362  snelpwg  5396  ordtri3  6360  ordsssuc  6415  iota1  6478  funbrfv2b  6898  dffn5  6899  feqmptdf  6911  unima  6916  dmfco  6937  fneqeql  6999  f1ompt  7064  dff13  7209  fliftcnv  7266  soisores  7282  isotr  7291  isoini  7293  caovord3  7580  releldm2  7996  fimaproj  8085  brtpos  8185  tpostpos  8196  oe1m  8480  oawordri  8485  oalimcl  8495  omlimcl  8513  omabs  8587  iserd  8670  qliftel  8747  qliftfun  8749  qliftf  8752  ecopovsym  8766  pw2f1olem  9019  mapen  9079  findcard3  9193  tfsnfin2  9273  suppeqfsuppbi  9292  mapfien  9321  supisolem  9387  cantnflem1  9610  wemapwe  9618  rankr1clem  9744  rankr1c  9745  ranklim  9768  r1pwALT  9770  r1pwcl  9771  isfin1-2  10307  isfin1-4  10309  fin71num  10319  axdc3lem2  10373  infinfg  10488  ltmnq  10895  prlem936  10970  ltsosr  11017  ltasr  11023  xrlenlt  11210  ltxrlt  11216  letri3  11231  ne0gt0  11251  subadd  11396  ltsubadd2  11621  lesubadd2  11623  suble  11628  ltsub23  11630  ltaddpos2  11641  ltsubpos  11642  subge02  11666  ltord2  11679  leord2  11680  ltaddsublt  11777  divmul  11812  divmul3  11814  rec11r  11854  ltdiv1  12020  ltdivmul2  12033  ledivmul2  12035  ltrec  12038  ltdiv2  12042  negfi  12105  negiso  12136  nnle1eq1  12207  avgle1  12417  avgle2  12418  avgle  12419  nn0le0eq0  12465  elz2  12542  znnnlt1  12554  zleltp1  12578  difrp  12982  xrltlen  13097  dfle2  13098  xrletri3  13105  xgepnf  13117  xlemnf  13119  qbtwnre  13151  xltnegi  13168  supxrre  13279  infxrre  13289  elioo5  13356  elfz5  13470  elfzm11  13549  predfz  13607  flbi  13775  flbi2  13776  fldiv4lem1div2uz2  13795  fznnfl  13821  zmodid2  13858  2submod  13894  lt2sq  14095  le2sq  14096  sqlecan  14171  bcval5  14280  pfxsuffeqwrdeq  14660  shftfib  15034  mulre  15083  cnpart  15202  01sqrexlem6  15209  sqrmo  15213  elicc4abs  15282  abs2difabs  15297  cau4  15319  limsupgre  15443  clim2  15466  ello1mpt2  15484  lo1resb  15526  o1resb  15528  climeq  15529  climmpt2  15535  isercoll  15630  caucvgb  15642  fsumabs  15764  isumshft  15804  geomulcvg  15841  absefib  16165  dvdsval3  16225  addmulmodb  16234  dvdsabseq  16282  dvdsflip  16286  dvdsssfz1  16287  mod2eq1n2dvds  16316  ndvdsadd  16379  bitscmp  16407  smupvallem  16452  dvdssq  16536  lcmdvds  16577  ncoprmgcdgt1b  16620  isprm3  16652  isprm5  16677  phiprmpw  16746  prmdiv  16755  pc11  16851  pcz  16852  pockthlem  16876  prmreclem2  16888  prmreclem4  16890  prmreclem6  16892  1arith  16898  vdwapun  16945  rami  16986  ramcl  17000  pwsle  17456  ercpbllem  17512  invsym  17729  funcres2c  17870  latnle  18439  grpinvcnv  18982  subgacs  19136  eqger  19153  ghmqusker  19262  gexdvds2  19560  pgpfi1  19570  pgpfi  19580  lsmass  19644  lssnle  19649  lsmdisj3b  19665  lsmhash  19680  ablsubadd  19784  gsumval3lem2  19881  subgdmdprd  20011  pgpfac1lem2  20052  dvdsr02  20352  issubrg3  20577  isdomn3  20692  drngid2  20729  sdrgunit  20773  sdrgacs  20778  lssacs  20962  prmirred  21454  chrdvds  21506  chrcong  21507  chrnzr  21510  znleval  21534  znleval2  21535  cygznlem3  21549  frlmbas  21735  elfilspd  21783  lindfmm  21807  islindf4  21818  islindf5  21819  psrbaglefi  21906  coe1mul2lem1  22232  mdetunilem9  22585  isneip  23070  neiptopnei  23097  lpdifsn  23108  restopnb  23140  restopn2  23142  restdis  23143  restperf  23149  lmbr2  23224  cncls2  23238  cnprest  23254  cnprest2  23255  iscnrm2  23303  ist0-2  23309  ist1-3  23314  ishaus2  23316  cmpfi  23373  dfconn2  23384  1stccnp  23427  subislly  23446  hausmapdom  23465  tx1cn  23574  tx2cn  23575  txcnmpt  23589  txrest  23596  hauseqlcld  23611  tgqtop  23677  qtopcld  23678  ordthmeolem  23766  trfil2  23852  trfil3  23853  trnei  23857  ufildr  23896  fmfg  23914  rnelfm  23918  fmfnfm  23923  elflim  23936  flimrest  23948  cnflf  23967  cnflf2  23968  ptcmplem2  24018  ghmcnp  24080  tsmssubm  24108  iscfilu  24252  xmetgt0  24323  prdsxmetlem  24333  blcomps  24358  blcom  24359  xblpnfps  24360  xblpnf  24361  blpnf  24362  xmeter  24398  setsxms  24444  imasf1obl  24453  stdbdbl  24482  metrest  24489  metuel2  24530  dscopn  24538  xrtgioo  24772  metdstri  24817  cnmpopc  24895  iihalf2  24900  icopnfhmeo  24910  evth2  24927  lmmbr3  25227  iscau3  25245  metcld  25273  cfilucfil3  25287  srabn  25327  rrxmet  25375  minveclem4  25399  evthicc2  25427  ovolgelb  25447  shft2rab  25475  ovolshftlem1  25476  sca2rab  25479  ovolscalem1  25480  ioombl1lem4  25528  mbfmulc2lem  25614  ismbf3d  25621  mbfsup  25631  mbfinf  25632  i1f1lem  25656  i1fmulclem  25669  mbfi1fseqlem4  25685  itg2seq  25709  ditgneg  25824  limcdif  25843  limcnlp  25845  cnplimc  25854  rolle  25957  mvth  25959  dvne0  25978  lhop1lem  25980  itgsubst  26016  mdegle0  26042  deg1leb  26060  deg1le0  26076  q1peqb  26121  coemulhi  26219  dgrlt  26231  plydivlem3  26261  vieta1lem2  26277  aannenlem1  26294  ulmres  26353  reefiso  26413  pilem3  26418  ellogdm  26603  root1eq1  26719  angpieqvdlem  26792  angpieqvdlem2  26793  quad2  26803  1cubr  26806  quart  26825  rlimcnp  26929  wilthlem2  27032  isppw  27077  dvdsflsumcom  27151  fsumvma  27176  logfac2  27180  chpchtsum  27182  dchrmulcl  27212  dchrresb  27222  bclbnd  27243  bposlem1  27247  bposlem5  27251  gausslemma2dlem0c  27321  lgsquadlem1  27343  m1lgs  27351  2lgsoddprmlem2  27372  dchrisumlem3  27454  dchrisum0lem1  27479  ltsval2  27620  noextenddif  27632  lesloe  27718  lestri3  27719  eqcuts  27777  elmade2  27850  ltadds1  27984  negsunif  28047  ltsubs1  28068  ltsubadds2d  28082  mulsproplem12  28119  ltmuls2  28163  ltmuls1d  28165  divmulsw  28185  ltdivmuls2wd  28192  oniso  28263  n0subs  28355  n0lesltp1  28358  elzn0s  28390  avglts1d  28445  avglts2d  28446  bdaypw2n0bndlem  28455  z12sge0  28475  dfz12s2  28480  elreno2  28487  tgjustr  28542  trgcgrg  28583  lnrot1  28691  islnopp  28807  ismidb  28846  islmib  28855  axsegconlem6  28991  axeuclidlem  29031  axcontlem2  29034  axcontlem4  29036  axcontlem12  29044  ausgrusgrb  29234  nb3grpr2  29452  cplgr2v  29501  umgr2v2enb1  29595  crctcsh  29892  clwwlknonwwlknonb  30176  eupth2lems  30308  nmoreltpnf  30840  isblo2  30854  nmlnogt0  30868  phoeqi  30928  ubthlem2  30942  hire  31165  normgt0  31198  ho01i  31899  ho02i  31900  hoeq1  31901  hoeq2  31902  nmopreltpnf  31940  adjeq  32006  leop  32194  leopmul2i  32206  pjnormssi  32239  pjimai  32247  jplem1  32339  mddmd2  32380  mdslmd1lem1  32396  mdslmd1lem2  32397  superpos  32425  atnssm0  32447  dmdbr5ati  32493  disjunsn  32664  fcoinvbr  32675  ofpreima  32738  funcnv5mpt  32740  suppiniseg  32759  isoun  32775  fpwrelmapffslem  32805  fpwrelmap  32806  iocinioc2  32852  xrdifh  32853  nndiffz1  32859  sgn3da  32907  xdivmul  32984  cntzsnid  33141  cntrval2  33232  isarchi2  33246  erler  33326  elrsp  33432  lsmsnpridl  33458  lsmssass  33462  r1pid2OLD  33669  esplyind  33719  finexttrb  33809  algextdeglem6  33866  algextdeglem7  33867  smatrcl  33940  rhmpreimacnlem  34028  sqsscirc2  34053  xrmulc1cn  34074  esumfsup  34214  1stmbfm  34404  2ndmbfm  34405  mbfmcnt  34412  eulerpartlems  34504  eulerpartlemd  34510  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemsima  34660  ballotlemfrcn0  34674  reprinfz1  34766  reprdifc  34771  bnj1173  35144  fineqvnttrclse  35268  vonf1owev  35290  zltp1ne  35292  lfuhgr2  35301  erdszelem7  35379  erdszelem9  35381  iscvm  35441  cvmlift3lem4  35504  rexxfr3dALT  35821  fscgr  36262  seglelin  36298  btwnoutside  36307  lineunray  36329  cldbnd  36508  isfne4  36522  fneval  36534  filnetlem4  36563  nndivsub  36639  bj-gabima  37247  dfgcd3  37638  fvineqsneu  37727  wl-sbhbt  37879  wl-sbcom2d  37886  wl-sbalnae  37887  sin2h  37931  cos2h  37932  matunitlindflem1  37937  matunitlindflem2  37938  matunitlindf  37939  ptrest  37940  poimirlem3  37944  poimirlem4  37945  poimirlem22  37963  poimirlem27  37968  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  itg2addnclem  37992  itg2addnclem2  37993  itg2gt0cn  37996  iblabsnclem  38004  ftc1anclem6  38019  areacirclem2  38030  areacirclem5  38033  areacirc  38034  mettrifi  38078  drngoi  38272  eldm4  38602  exanres2  38624  disjecxrn  38733  exeupre  38812  brcoss2  38843  br1cossres2  38851  eldmcoss2  38870  eldm1cossres2  38872  brcosscnv2  38884  erimeq2  39084  disjqmap  39148  disjlem19  39225  prter3  39328  islshpat  39463  lsatnle  39490  ellkr2  39537  lshpkr  39563  lkr0f2  39607  lduallkr3  39608  lkreqN  39616  cvrval2  39720  isat3  39753  glbconN  39823  hlrelat5N  39847  cvrval4N  39860  atlt  39883  1cvrco  39918  pmaple  40207  isline2  40220  isline4N  40223  elpaddn0  40246  elpadd2at2  40253  cdlemkid4  41380  dia0  41498  cdlemm10N  41564  dibglbN  41612  dihmeetlem4preN  41752  dochkrshp3  41834  dvh4dimlem  41889  lcfl5  41942  mapdpglem3  42121  mapdheq  42174  hdmap1eq  42247  hdmapval2lem  42277  hdmapoc  42377  hlhillcs  42404  lcmineqlem18  42485  dvdsexpb  42767  renegadd  42804  resubadd  42811  redivmuld  42877  mulgt0b1d  42917  fsuppssind  43026  fz1eqin  43201  diophin  43204  jm2.19  43421  rmxdiophlem  43443  pw2f1ocnv  43465  wepwsolem  43470  gicabl  43527  idomodle  43619  onsupmaxb  43667  cantnf2  43753  tfsconcatb0  43772  tfsnfin  43780  ntrclsfveq2  44488  ntrclsss  44490  ntrclsk4  44499  extoimad  44591  radcnvrat  44741  bcc0  44767  supxrre3rnmpt  45857  clim2f  46064  clim2f2  46098  liminfreuzlem  46230  liminfltlem  46232  xlimmnflimsup2  46280  xlimpnfliminf2  46289  xlimlimsupleliminf  46291  opprb  47473  funbrafv2b  47601  dfafn5a  47602  leaddsuble  47739  mod2addne  47812  iccpartgtprec  47874  flsqrt  48050  dfeven2  48119  dfodd3  48120  lindslinindimp2lem4  48931  snlindsntor  48941  regt1loggt0  49006  elbigo2  49022  elbigolo1  49027  fldivexpfllog2  49035  nnlog2ge0lt1  49036  blenpw2m1  49049  naryfvalelwrdf  49103  isprsd  49424  resccatlem  49542  functhinclem1  49913  thincciso  49922  thinciso  49939  isinito2lem  49967  fulltermc  49980  prstcprs  50029  oduoppcciso  50035  postc  50038  lmdran  50140  cmdlan  50141