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  5354  snelpwg  5388  ordtri3  6351  ordsssuc  6406  iota1  6469  funbrfv2b  6889  dffn5  6890  feqmptdf  6902  unima  6907  dmfco  6928  fneqeql  6990  f1ompt  7055  dff13  7200  fliftcnv  7257  soisores  7273  isotr  7282  isoini  7284  caovord3  7571  releldm2  7987  fimaproj  8076  brtpos  8176  tpostpos  8187  oe1m  8471  oawordri  8476  oalimcl  8486  omlimcl  8504  omabs  8578  iserd  8661  qliftel  8738  qliftfun  8740  qliftf  8743  ecopovsym  8757  pw2f1olem  9010  mapen  9070  findcard3  9184  tfsnfin2  9264  suppeqfsuppbi  9283  mapfien  9312  supisolem  9378  cantnflem1  9599  wemapwe  9607  rankr1clem  9733  rankr1c  9734  ranklim  9757  r1pwALT  9759  r1pwcl  9760  isfin1-2  10296  isfin1-4  10298  fin71num  10308  axdc3lem2  10362  infinfg  10477  ltmnq  10884  prlem936  10959  ltsosr  11006  ltasr  11012  xrlenlt  11198  ltxrlt  11204  letri3  11219  ne0gt0  11239  subadd  11384  ltsubadd2  11609  lesubadd2  11611  suble  11616  ltsub23  11618  ltaddpos2  11629  ltsubpos  11630  subge02  11654  ltord2  11667  leord2  11668  ltaddsublt  11765  divmul  11800  divmul3  11802  rec11r  11841  ltdiv1  12007  ltdivmul2  12020  ledivmul2  12022  ltrec  12025  ltdiv2  12029  negfi  12092  negiso  12123  nnle1eq1  12176  avgle1  12382  avgle2  12383  avgle  12384  nn0le0eq0  12430  elz2  12507  znnnlt1  12519  zleltp1  12543  difrp  12946  xrltlen  13061  dfle2  13062  xrletri3  13069  xgepnf  13081  xlemnf  13083  qbtwnre  13115  xltnegi  13132  supxrre  13243  infxrre  13253  elioo5  13320  elfz5  13433  elfzm11  13512  predfz  13570  flbi  13737  flbi2  13738  fldiv4lem1div2uz2  13757  fznnfl  13783  zmodid2  13820  2submod  13856  lt2sq  14057  le2sq  14058  sqlecan  14133  bcval5  14242  pfxsuffeqwrdeq  14622  shftfib  14996  mulre  15045  cnpart  15164  01sqrexlem6  15171  sqrmo  15175  elicc4abs  15244  abs2difabs  15259  cau4  15281  limsupgre  15405  clim2  15428  ello1mpt2  15446  lo1resb  15488  o1resb  15490  climeq  15491  climmpt2  15497  isercoll  15592  caucvgb  15604  fsumabs  15725  isumshft  15763  geomulcvg  15800  absefib  16124  dvdsval3  16184  addmulmodb  16193  dvdsabseq  16241  dvdsflip  16245  dvdsssfz1  16246  mod2eq1n2dvds  16275  ndvdsadd  16338  bitscmp  16366  smupvallem  16411  dvdssq  16495  lcmdvds  16536  ncoprmgcdgt1b  16579  isprm3  16611  isprm5  16635  phiprmpw  16704  prmdiv  16713  pc11  16809  pcz  16810  pockthlem  16834  prmreclem2  16846  prmreclem4  16848  prmreclem6  16850  1arith  16856  vdwapun  16903  rami  16944  ramcl  16958  pwsle  17414  ercpbllem  17470  invsym  17687  funcres2c  17828  latnle  18397  grpinvcnv  18940  subgacs  19094  eqger  19111  ghmqusker  19220  gexdvds2  19518  pgpfi1  19528  pgpfi  19538  lsmass  19602  lssnle  19607  lsmdisj3b  19623  lsmhash  19638  ablsubadd  19742  gsumval3lem2  19839  subgdmdprd  19969  pgpfac1lem2  20010  dvdsr02  20310  issubrg3  20535  isdomn3  20650  drngid2  20687  sdrgunit  20731  sdrgacs  20736  lssacs  20920  prmirred  21431  chrdvds  21483  chrcong  21484  chrnzr  21487  znleval  21511  znleval2  21512  cygznlem3  21526  frlmbas  21712  elfilspd  21760  lindfmm  21784  islindf4  21795  islindf5  21796  psrbaglefi  21883  coe1mul2lem1  22210  mdetunilem9  22563  isneip  23048  neiptopnei  23075  lpdifsn  23086  restopnb  23118  restopn2  23120  restdis  23121  restperf  23127  lmbr2  23202  cncls2  23216  cnprest  23232  cnprest2  23233  iscnrm2  23281  ist0-2  23287  ist1-3  23292  ishaus2  23294  cmpfi  23351  dfconn2  23362  1stccnp  23405  subislly  23424  hausmapdom  23443  tx1cn  23552  tx2cn  23553  txcnmpt  23567  txrest  23574  hauseqlcld  23589  tgqtop  23655  qtopcld  23656  ordthmeolem  23744  trfil2  23830  trfil3  23831  trnei  23835  ufildr  23874  fmfg  23892  rnelfm  23896  fmfnfm  23901  elflim  23914  flimrest  23926  cnflf  23945  cnflf2  23946  ptcmplem2  23996  ghmcnp  24058  tsmssubm  24086  iscfilu  24230  xmetgt0  24301  prdsxmetlem  24311  blcomps  24336  blcom  24337  xblpnfps  24338  xblpnf  24339  blpnf  24340  xmeter  24376  setsxms  24422  imasf1obl  24431  stdbdbl  24460  metrest  24467  metuel2  24508  dscopn  24516  xrtgioo  24750  metdstri  24795  cnmpopc  24873  iihalf2  24878  icopnfhmeo  24888  evth2  24905  lmmbr3  25205  iscau3  25223  metcld  25251  cfilucfil3  25265  srabn  25305  rrxmet  25353  minveclem4  25377  evthicc2  25405  ovolgelb  25425  shft2rab  25453  ovolshftlem1  25454  sca2rab  25457  ovolscalem1  25458  ioombl1lem4  25506  mbfmulc2lem  25592  ismbf3d  25599  mbfsup  25609  mbfinf  25610  i1f1lem  25634  i1fmulclem  25647  mbfi1fseqlem4  25663  itg2seq  25687  ditgneg  25802  limcdif  25821  limcnlp  25823  cnplimc  25832  rolle  25935  mvth  25938  dvne0  25957  lhop1lem  25959  itgsubst  25997  mdegle0  26023  deg1leb  26041  deg1le0  26057  q1peqb  26102  coemulhi  26200  dgrlt  26212  plydivlem3  26243  vieta1lem2  26259  aannenlem1  26276  ulmres  26337  reefiso  26398  pilem3  26403  ellogdm  26588  root1eq1  26705  angpieqvdlem  26778  angpieqvdlem2  26779  quad2  26789  1cubr  26792  quart  26811  rlimcnp  26915  wilthlem2  27019  isppw  27064  dvdsflsumcom  27138  fsumvma  27164  logfac2  27168  chpchtsum  27170  dchrmulcl  27200  dchrresb  27210  bclbnd  27231  bposlem1  27235  bposlem5  27239  gausslemma2dlem0c  27309  lgsquadlem1  27331  m1lgs  27339  2lgsoddprmlem2  27360  dchrisumlem3  27442  dchrisum0lem1  27467  ltsval2  27608  noextenddif  27620  lesloe  27706  lestri3  27707  eqcuts  27765  elmade2  27838  ltadds1  27972  negsunif  28035  ltsubs1  28056  ltsubadds2d  28070  mulsproplem12  28107  ltmuls2  28151  ltmuls1d  28153  divmulsw  28173  ltdivmuls2wd  28180  oniso  28251  n0subs  28343  n0lesltp1  28346  elzn0s  28378  avglts1d  28433  avglts2d  28434  bdaypw2n0bndlem  28443  z12sge0  28463  dfz12s2  28468  elreno2  28475  tgjustr  28530  trgcgrg  28571  lnrot1  28679  islnopp  28795  ismidb  28834  islmib  28843  axsegconlem6  28979  axeuclidlem  29019  axcontlem2  29022  axcontlem4  29024  axcontlem12  29032  ausgrusgrb  29222  nb3grpr2  29440  cplgr2v  29489  umgr2v2enb1  29584  crctcsh  29881  clwwlknonwwlknonb  30165  eupth2lems  30297  nmoreltpnf  30829  isblo2  30843  nmlnogt0  30857  phoeqi  30917  ubthlem2  30931  hire  31154  normgt0  31187  ho01i  31888  ho02i  31889  hoeq1  31890  hoeq2  31891  nmopreltpnf  31929  adjeq  31995  leop  32183  leopmul2i  32195  pjnormssi  32228  pjimai  32236  jplem1  32328  mddmd2  32369  mdslmd1lem1  32385  mdslmd1lem2  32386  superpos  32414  atnssm0  32436  dmdbr5ati  32482  disjunsn  32653  fcoinvbr  32664  ofpreima  32727  funcnv5mpt  32729  suppiniseg  32748  isoun  32764  fpwrelmapffslem  32794  fpwrelmap  32795  iocinioc2  32842  xrdifh  32843  nndiffz1  32849  sgn3da  32898  xdivmul  32989  cntzsnid  33146  cntrval2  33237  isarchi2  33251  erler  33331  elrsp  33437  lsmsnpridl  33463  lsmssass  33467  r1pid2OLD  33674  esplyind  33724  finexttrb  33815  algextdeglem6  33872  algextdeglem7  33873  smatrcl  33946  rhmpreimacnlem  34034  sqsscirc2  34059  xrmulc1cn  34080  esumfsup  34220  1stmbfm  34410  2ndmbfm  34411  mbfmcnt  34418  eulerpartlems  34510  eulerpartlemd  34516  ballotlemfc0  34643  ballotlemfcc  34644  ballotlemsima  34666  ballotlemfrcn0  34680  reprinfz1  34772  reprdifc  34777  bnj1173  35150  fineqvnttrclse  35274  vonf1owev  35296  zltp1ne  35298  lfuhgr2  35307  erdszelem7  35385  erdszelem9  35387  iscvm  35447  cvmlift3lem4  35510  rexxfr3dALT  35827  fscgr  36268  seglelin  36304  btwnoutside  36313  lineunray  36335  cldbnd  36514  isfne4  36528  fneval  36540  filnetlem4  36569  nndivsub  36645  bj-gabima  37245  dfgcd3  37636  fvineqsneu  37723  wl-sbhbt  37870  wl-sbcom2d  37877  wl-sbalnae  37878  sin2h  37922  cos2h  37923  matunitlindflem1  37928  matunitlindflem2  37929  matunitlindf  37930  ptrest  37931  poimirlem3  37935  poimirlem4  37936  poimirlem22  37954  poimirlem27  37959  mblfinlem3  37971  mblfinlem4  37972  ismblfin  37973  itg2addnclem  37983  itg2addnclem2  37984  itg2gt0cn  37987  iblabsnclem  37995  ftc1anclem6  38010  areacirclem2  38021  areacirclem5  38024  areacirc  38025  mettrifi  38069  drngoi  38263  eldm4  38593  exanres2  38615  disjecxrn  38724  exeupre  38803  brcoss2  38834  br1cossres2  38842  eldmcoss2  38861  eldm1cossres2  38863  brcosscnv2  38875  erimeq2  39075  disjqmap  39139  disjlem19  39216  prter3  39319  islshpat  39454  lsatnle  39481  ellkr2  39528  lshpkr  39554  lkr0f2  39598  lduallkr3  39599  lkreqN  39607  cvrval2  39711  isat3  39744  glbconN  39814  hlrelat5N  39838  cvrval4N  39851  atlt  39874  1cvrco  39909  pmaple  40198  isline2  40211  isline4N  40214  elpaddn0  40237  elpadd2at2  40244  cdlemkid4  41371  dia0  41489  cdlemm10N  41555  dibglbN  41603  dihmeetlem4preN  41743  dochkrshp3  41825  dvh4dimlem  41880  lcfl5  41933  mapdpglem3  42112  mapdheq  42165  hdmap1eq  42238  hdmapval2lem  42268  hdmapoc  42368  hlhillcs  42395  lcmineqlem18  42477  dvdsexpb  42766  renegadd  42803  resubadd  42810  redivmuld  42876  mulgt0b1d  42916  fsuppssind  43025  fz1eqin  43200  diophin  43203  jm2.19  43424  rmxdiophlem  43446  pw2f1ocnv  43468  wepwsolem  43473  gicabl  43530  idomodle  43622  onsupmaxb  43670  cantnf2  43756  tfsconcatb0  43775  tfsnfin  43783  ntrclsfveq2  44491  ntrclsss  44493  ntrclsk4  44502  extoimad  44594  radcnvrat  44744  bcc0  44770  supxrre3rnmpt  45861  clim2f  46068  clim2f2  46102  liminfreuzlem  46234  liminfltlem  46236  xlimmnflimsup2  46284  xlimpnfliminf2  46293  xlimlimsupleliminf  46295  opprb  47465  funbrafv2b  47593  dfafn5a  47594  leaddsuble  47731  mod2addne  47798  iccpartgtprec  47854  flsqrt  48027  dfeven2  48083  dfodd3  48084  lindslinindimp2lem4  48895  snlindsntor  48905  regt1loggt0  48970  elbigo2  48986  elbigolo1  48991  fldivexpfllog2  48999  nnlog2ge0lt1  49000  blenpw2m1  49013  naryfvalelwrdf  49067  isprsd  49388  resccatlem  49506  functhinclem1  49877  thincciso  49886  thinciso  49903  isinito2lem  49931  fulltermc  49944  prstcprs  49993  oduoppcciso  49999  postc  50002  lmdran  50104  cmdlan  50105