Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  bibi12d Structured version   Visualization version   GIF version

Theorem bibi12d 349
 Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 26-May-1993.)
Hypotheses
Ref Expression
imbi12d.1 (𝜑 → (𝜓𝜒))
imbi12d.2 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
bibi12d (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))

Proof of Theorem bibi12d
StepHypRef Expression
1 imbi12d.1 . . 3 (𝜑 → (𝜓𝜒))
21bibi1d 347 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 imbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43bibi2d 346 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 282 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  bi2bian9  640  xorbi12d  1518  norass  1534  sbbib  2372  sb8eulem  2662  abbi  2868  cleqh  2916  cleqf  2986  vtoclb  3515  vtoclbg  3520  ceqsexg  3597  elabgf  3613  elabg  3617  reu6  3668  ru  3722  sbcbig  3773  unineq  4207  sbcnestgfw  4329  sbcnestgf  4334  preq12bg  4747  axrep1  5158  axrep4  5162  nalset  5184  opthg  5337  opelopabsb  5385  isso2i  5476  opeliunxp2  5677  resieq  5833  elimasng  5926  cbviotaw  6294  cbviota  6296  iota2df  6315  fnbrfvb  6697  fvelimab  6716  fvopab5  6781  fmptco  6872  fsng  6880  fressnfv  6903  fnpr2g  6954  isorel  7062  isocnv  7066  isocnv3  7068  isotr  7072  ovg  7297  caovcang  7333  caovordg  7339  caovord3d  7342  caovord  7343  orduninsuc  7542  opeliunxp2f  7863  brtpos  7888  dftpos4  7898  omopth  8272  ecopovsym  8386  xpf1o  8667  nneneq  8688  r1pwALT  9263  karden  9312  infxpenlem  9428  aceq0  9533  cflim2  9678  zfac  9875  ttukeylem1  9924  axextnd  10006  axrepndlem1  10007  axrepndlem2  10008  axrepnd  10009  axacndlem5  10026  zfcndrep  10029  zfcndac  10034  winalim  10110  gruina  10233  ltrnq  10394  ltsosr  10509  ltasr  10515  axpre-lttri  10580  axpre-ltadd  10582  nn0sub  11939  zextle  12047  zextlt  12048  xlesubadd  12648  sqeqor  13578  nn0opth2  13632  rexfiuz  14703  climshft  14929  rpnnen2lem10  15572  dvdsext  15667  ltoddhalfle  15706  halfleoddlt  15707  sumodd  15733  sadcadd  15801  dvdssq  15905  rpexp  16058  pcdvdsb  16199  imasleval  16810  isacs2  16920  acsfiel  16921  funcres2b  17163  pospropd  17740  isnsg  18303  nsgbi  18305  elnmz  18311  nmzbi  18312  oddvdsnn0  18668  odeq  18674  odmulg  18679  isslw  18729  slwispgp  18732  gsumval3lem2  19023  gsumcom2  19092  abveq0  19594  cnt0  21955  kqfvima  22339  kqt0lem  22345  isr0  22346  r0cld  22347  regr1lem2  22349  nrmr0reg  22358  isfildlem  22466  cnextfvval  22674  xmeteq0  22949  imasf1oxmet  22986  comet  23124  dscmet  23183  nrmmetd  23185  tngngp  23264  tngngp3  23266  mbfsup  24272  mbfinf  24273  degltlem1  24677  logltb  25195  cxple2  25292  rlimcnp  25555  rlimcnp2  25556  isppw2  25704  sqf11  25728  tgjustc1  26273  tgjustc2  26274  f1otrgitv  26668  nbuhgr2vtx1edgb  27146  dfconngr1  27977  eupth2lem3lem6  28022  nmlno0i  28581  nmlno0  28582  blocn  28594  ubth  28660  hvsubeq0  28855  hvaddcan  28857  hvsubadd  28864  normsub0  28923  hlim2  28979  pjoc1  29221  pjoc2  29226  chne0  29281  chsscon3  29287  chlejb1  29299  chnle  29301  h1de2ci  29343  elspansn  29353  elspansn2  29354  cmbr3  29395  cmcm  29401  cmcm3  29402  pjch1  29457  pjch  29481  pj11  29501  pjnel  29513  eigorth  29625  elnlfn  29715  nmlnop0  29785  lnopeq  29796  lnopcon  29822  lnfncon  29843  pjdifnormi  29954  chrelat2  30157  cvexch  30161  mdsym  30199  fmptcof2  30424  mgcoval  30698  mgcval  30699  mgccole1  30702  mgccole2  30703  mcgmnt1  30704  mcgmnt2  30705  mcgcnv  30709  ist0cld  31190  zarclssn  31230  zart0  31236  signswch  31945  cvmlift2lem12  32675  cvmlift2lem13  32676  satfv1lem  32723  satf0op  32738  fmlafvel  32746  abs2sqle  33037  abs2sqlt  33038  dfpo2  33105  eqfunresadj  33118  axextdist  33158  slerec  33391  brimageg  33502  brdomaing  33510  brrangeg  33511  elhf2  33750  nn0prpwlem  33784  nn0prpw  33785  onsuct0  33903  bj-sbceqgALT  34344  bj-ru0  34378  dfgcd3  34739  cbveud  34790  wl-3xorbi123d  34891  matunitlindf  35054  prdsbnd2  35232  isdrngo1  35393  eqrelf  35676  elsymrels5  35951  dfdisjs5  36104  eldisjs5  36118  lsatcmp  36298  llnexchb2  37164  lautset  37377  lautle  37379  zindbi  39884  wepwsolem  39983  aomclem8  40002  ntrneik13  40798  ntrneix13  40799  ntrneik4w  40800  2sbc6g  41116  2sbc5g  41117  wessf1ornlem  41808  fourierdlem31  42777  fourierdlem42  42788  fourierdlem54  42799  funressndmafv2rn  43776  dfatbrafv2b  43798  fnbrafv2b  43801  ichbidv  43967  ichnfim  43978  sprsymrelf  44009  sprsymrelfo  44011  isomuspgrlem2b  44344  isomuspgrlem2d  44346  line2ylem  45162  line2xlem  45164
 Copyright terms: Public domain W3C validator