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  2479  sbcom3  2509  sbal1  2531  sbal2  2532  2reu4lem  4453  issn  4765  disjprg  5070  reuhypd  5350  snelpwg  5384  ordtri3  6348  ordsssuc  6403  iota1  6466  funbrfv2b  6886  dffn5  6887  feqmptdf  6899  unima  6904  dmfco  6925  fneqeql  6987  f1ompt  7052  dff13  7198  fliftcnv  7255  soisores  7271  isotr  7280  isoini  7282  caovord3  7569  releldm2  7985  fimaproj  8074  brtpos  8174  tpostpos  8185  oe1m  8469  oawordri  8474  oalimcl  8484  omlimcl  8502  omabs  8576  iserd  8659  qliftel  8736  qliftfun  8738  qliftf  8741  ecopovsym  8755  pw2f1olem  9008  mapen  9068  findcard3  9182  tfsnfin2  9262  suppeqfsuppbi  9281  mapfien  9310  supisolem  9376  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  11199  ltxrlt  11205  letri3  11220  ne0gt0  11240  subadd  11385  ltsubadd2  11610  lesubadd2  11612  suble  11617  ltsub23  11619  ltaddpos2  11630  ltsubpos  11631  subge02  11655  ltord2  11668  leord2  11669  ltaddsublt  11766  divmul  11801  divmul3  11803  rec11r  11843  ltdiv1  12009  ltdivmul2  12022  ledivmul2  12024  ltrec  12027  ltdiv2  12031  negfi  12094  negiso  12125  nnle1eq1  12196  avgle1  12406  avgle2  12407  avgle  12408  nn0le0eq0  12454  elz2  12531  znnnlt1  12543  zleltp1  12567  difrp  12971  xrltlen  13086  dfle2  13087  xrletri3  13094  xgepnf  13106  xlemnf  13108  qbtwnre  13140  xltnegi  13157  supxrre  13268  infxrre  13278  elioo5  13345  elfz5  13459  elfzm11  13538  predfz  13596  flbi  13764  flbi2  13765  fldiv4lem1div2uz2  13784  fznnfl  13810  zmodid2  13847  2submod  13883  lt2sq  14084  le2sq  14085  sqlecan  14160  bcval5  14269  pfxsuffeqwrdeq  14649  shftfib  15023  mulre  15072  cnpart  15191  01sqrexlem6  15198  sqrmo  15202  elicc4abs  15271  abs2difabs  15286  cau4  15308  limsupgre  15432  clim2  15455  ello1mpt2  15473  lo1resb  15515  o1resb  15517  climeq  15518  climmpt2  15524  isercoll  15619  caucvgb  15631  fsumabs  15753  isumshft  15793  geomulcvg  15830  absefib  16154  dvdsval3  16214  addmulmodb  16223  dvdsabseq  16271  dvdsflip  16275  dvdsssfz1  16276  mod2eq1n2dvds  16305  ndvdsadd  16368  bitscmp  16396  smupvallem  16441  dvdssq  16525  lcmdvds  16566  ncoprmgcdgt1b  16609  isprm3  16641  isprm5  16666  phiprmpw  16735  prmdiv  16744  pc11  16840  pcz  16841  pockthlem  16865  prmreclem2  16877  prmreclem4  16879  prmreclem6  16881  1arith  16887  vdwapun  16934  rami  16975  ramcl  16989  pwsle  17445  ercpbllem  17501  invsym  17718  funcres2c  17859  latnle  18428  grpinvcnv  18971  subgacs  19125  eqger  19142  ghmqusker  19251  gexdvds2  19549  pgpfi1  19559  pgpfi  19569  lsmass  19633  lssnle  19638  lsmdisj3b  19654  lsmhash  19669  ablsubadd  19773  gsumval3lem2  19870  subgdmdprd  20000  pgpfac1lem2  20041  dvdsr02  20341  issubrg3  20566  isdomn3  20681  drngid2  20718  sdrgunit  20762  sdrgacs  20767  lssacs  20951  prmirred  21443  chrdvds  21495  chrcong  21496  chrnzr  21499  znleval  21523  znleval2  21524  cygznlem3  21538  frlmbas  21724  elfilspd  21772  lindfmm  21796  islindf4  21807  islindf5  21808  psrbaglefi  21895  coe1mul2lem1  22220  mdetunilem9  22573  isneip  23058  neiptopnei  23085  lpdifsn  23096  restopnb  23128  restopn2  23130  restdis  23131  restperf  23137  lmbr2  23212  cncls2  23226  cnprest  23242  cnprest2  23243  iscnrm2  23291  ist0-2  23297  ist1-3  23302  ishaus2  23304  cmpfi  23361  dfconn2  23372  1stccnp  23415  subislly  23434  hausmapdom  23453  tx1cn  23562  tx2cn  23563  txcnmpt  23577  txrest  23584  hauseqlcld  23599  tgqtop  23665  qtopcld  23666  ordthmeolem  23754  trfil2  23840  trfil3  23841  trnei  23845  ufildr  23884  fmfg  23902  rnelfm  23906  fmfnfm  23911  elflim  23924  flimrest  23936  cnflf  23955  cnflf2  23956  ptcmplem2  24006  ghmcnp  24068  tsmssubm  24096  iscfilu  24240  xmetgt0  24311  prdsxmetlem  24321  blcomps  24346  blcom  24347  xblpnfps  24348  xblpnf  24349  blpnf  24350  xmeter  24386  setsxms  24432  imasf1obl  24441  stdbdbl  24470  metrest  24477  metuel2  24518  dscopn  24526  xrtgioo  24760  metdstri  24805  cnmpopc  24883  iihalf2  24888  icopnfhmeo  24898  evth2  24915  lmmbr3  25215  iscau3  25233  metcld  25261  cfilucfil3  25275  srabn  25315  rrxmet  25363  minveclem4  25387  evthicc2  25415  ovolgelb  25435  shft2rab  25463  ovolshftlem1  25464  sca2rab  25467  ovolscalem1  25468  ioombl1lem4  25516  mbfmulc2lem  25602  ismbf3d  25609  mbfsup  25619  mbfinf  25620  i1f1lem  25644  i1fmulclem  25657  mbfi1fseqlem4  25673  itg2seq  25697  ditgneg  25812  limcdif  25831  limcnlp  25833  cnplimc  25842  rolle  25945  mvth  25947  dvne0  25966  lhop1lem  25968  itgsubst  26004  mdegle0  26030  deg1leb  26048  deg1le0  26064  q1peqb  26109  coemulhi  26207  dgrlt  26219  plydivlem3  26249  vieta1lem2  26265  aannenlem1  26282  ulmres  26341  reefiso  26401  pilem3  26406  ellogdm  26591  root1eq1  26707  angpieqvdlem  26780  angpieqvdlem2  26781  quad2  26791  1cubr  26794  quart  26813  rlimcnp  26917  wilthlem2  27020  isppw  27065  dvdsflsumcom  27139  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  29583  crctcsh  29880  clwwlknonwwlknonb  30164  eupth2lems  30296  nmoreltpnf  30828  isblo2  30842  nmlnogt0  30856  phoeqi  30916  ubthlem2  30930  hire  31153  normgt0  31186  ho01i  31887  ho02i  31888  hoeq1  31889  hoeq2  31890  nmopreltpnf  31928  adjeq  31994  leop  32182  leopmul2i  32194  pjnormssi  32227  pjimai  32235  jplem1  32327  mddmd2  32368  mdslmd1lem1  32384  mdslmd1lem2  32385  superpos  32413  atnssm0  32435  dmdbr5ati  32481  disjunsn  32652  fcoinvbr  32663  ofpreima  32726  funcnv5mpt  32728  suppiniseg  32747  isoun  32763  fpwrelmapffslem  32793  fpwrelmap  32794  iocinioc2  32840  xrdifh  32841  nndiffz1  32847  sgn3da  32895  xdivmul  32972  cntzsnid  33129  cntrval2  33220  isarchi2  33234  erler  33314  elrsp  33420  lsmsnpridl  33446  lsmssass  33450  r1pid2OLD  33657  esplyind  33707  finexttrb  33797  algextdeglem6  33854  algextdeglem7  33855  smatrcl  33928  rhmpreimacnlem  34016  sqsscirc2  34041  xrmulc1cn  34062  esumfsup  34202  1stmbfm  34392  2ndmbfm  34393  mbfmcnt  34400  eulerpartlems  34492  eulerpartlemd  34498  ballotlemfc0  34625  ballotlemfcc  34626  ballotlemsima  34648  ballotlemfrcn0  34662  reprinfz1  34754  reprdifc  34759  bnj1173  35132  fineqvnttrclse  35256  vonf1owev  35278  zltp1ne  35280  lfuhgr2  35289  erdszelem7  35367  erdszelem9  35369  iscvm  35429  cvmlift3lem4  35492  rexxfr3dALT  35809  fscgr  36250  seglelin  36286  btwnoutside  36295  lineunray  36317  cldbnd  36496  isfne4  36510  fneval  36522  filnetlem4  36551  nndivsub  36627  bj-gabima  37235  dfgcd3  37626  fvineqsneu  37715  wl-sbhbt  37867  wl-sbcom2d  37874  wl-sbalnae  37875  sin2h  37919  cos2h  37920  matunitlindflem1  37925  matunitlindflem2  37926  matunitlindf  37927  ptrest  37928  poimirlem3  37932  poimirlem4  37933  poimirlem22  37951  poimirlem27  37956  mblfinlem3  37968  mblfinlem4  37969  ismblfin  37970  itg2addnclem  37980  itg2addnclem2  37981  itg2gt0cn  37984  iblabsnclem  37992  ftc1anclem6  38007  areacirclem2  38018  areacirclem5  38021  areacirc  38022  mettrifi  38066  drngoi  38260  eldm4  38590  exanres2  38612  disjecxrn  38721  exeupre  38800  brcoss2  38831  br1cossres2  38839  eldmcoss2  38858  eldm1cossres2  38860  brcosscnv2  38872  erimeq2  39072  disjqmap  39136  disjlem19  39213  prter3  39316  islshpat  39451  lsatnle  39478  ellkr2  39525  lshpkr  39551  lkr0f2  39595  lduallkr3  39596  lkreqN  39604  cvrval2  39708  isat3  39741  glbconN  39811  hlrelat5N  39835  cvrval4N  39848  atlt  39871  1cvrco  39906  pmaple  40195  isline2  40208  isline4N  40211  elpaddn0  40234  elpadd2at2  40241  cdlemkid4  41368  dia0  41486  cdlemm10N  41552  dibglbN  41600  dihmeetlem4preN  41740  dochkrshp3  41822  dvh4dimlem  41877  lcfl5  41930  mapdpglem3  42109  mapdheq  42162  hdmap1eq  42235  hdmapval2lem  42265  hdmapoc  42365  hlhillcs  42392  lcmineqlem18  42473  dvdsexpb  42755  renegadd  42792  resubadd  42799  redivmuld  42865  mulgt0b1d  42905  fsuppssind  43014  fz1eqin  43189  diophin  43192  jm2.19  43409  rmxdiophlem  43431  pw2f1ocnv  43453  wepwsolem  43458  gicabl  43515  idomodle  43607  onsupmaxb  43655  cantnf2  43741  tfsconcatb0  43760  tfsnfin  43768  ntrclsfveq2  44476  ntrclsss  44478  ntrclsk4  44487  extoimad  44579  radcnvrat  44729  bcc0  44755  supxrre3rnmpt  45845  clim2f  46052  clim2f2  46086  liminfreuzlem  46218  liminfltlem  46220  xlimmnflimsup2  46268  xlimpnfliminf2  46277  xlimlimsupleliminf  46279  opprb  47467  funbrafv2b  47595  dfafn5a  47596  leaddsuble  47733  mod2addne  47806  iccpartgtprec  47868  flsqrt  48044  dfeven2  48113  dfodd3  48114  lindslinindimp2lem4  48925  snlindsntor  48935  regt1loggt0  49000  elbigo2  49016  elbigolo1  49021  fldivexpfllog2  49029  nnlog2ge0lt1  49030  blenpw2m1  49043  naryfvalelwrdf  49097  isprsd  49418  resccatlem  49536  functhinclem1  49907  thincciso  49916  thinciso  49933  isinito2lem  49961  fulltermc  49974  prstcprs  50023  oduoppcciso  50029  postc  50032  lmdran  50134  cmdlan  50135