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

Theorem bibi12d 345
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 343 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 imbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43bibi2d 342 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 278 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
Colors of variables: wff setvar class
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:  bi2bian9  639  xorbi12d  1525  norass  1538  sbbib  2357  sb8eulem  2596  abbi  2808  cleqh  2867  clelab  2881  cleqf  2936  vtoclb  3520  vtoclbg  3526  ceqsexg  3601  elabgf  3624  elabgOLD  3627  reu6  3682  ru  3736  sbcbig  3791  unineq  4235  sbcnestgfw  4376  sbcnestgf  4381  preq12bg  4809  axrep1  5241  axrep4  5245  nalset  5268  opthg  5432  opelopabsb  5485  isso2i  5578  opeliunxp2  5792  resieq  5946  elimasngOLD  6040  dfpo2  6246  cbviotaw  6452  cbviota  6455  iota2df  6480  fnbrfvb  6892  fvelimab  6911  fvopab5  6977  fmptco  7071  fsng  7079  fressnfv  7102  fnpr2g  7156  isorel  7267  isocnv  7271  isocnv3  7273  isotr  7277  eqfunresadj  7301  ovg  7515  caovcang  7551  caovordg  7557  caovord3d  7560  caovord  7561  orduninsuc  7775  xpord2pred  8073  xpord3pred  8080  opeliunxp2f  8137  brtpos  8162  dftpos4  8172  omopth  8604  ecopovsym  8754  xpf1o  9079  nneneq  9149  nneneqOLD  9161  ttrclselem2  9658  r1pwALT  9778  karden  9827  infxpenlem  9945  aceq0  10050  cflim2  10195  zfac  10392  ttukeylem1  10441  axextnd  10523  axrepndlem1  10524  axrepndlem2  10525  axrepnd  10526  axacndlem5  10543  zfcndrep  10546  zfcndac  10551  winalim  10627  gruina  10750  ltrnq  10911  ltsosr  11026  ltasr  11032  axpre-lttri  11097  axpre-ltadd  11099  nn0sub  12459  zextle  12572  zextlt  12573  xlesubadd  13174  sqeqor  14112  nn0opth2  14164  rexfiuz  15224  climshft  15450  rpnnen2lem10  16097  dvdsext  16195  ltoddhalfle  16235  halfleoddlt  16236  sumodd  16262  sadcadd  16330  dvdssq  16435  rpexp  16590  pcdvdsb  16733  imasleval  17415  isacs2  17525  acsfiel  17526  funcres2b  17775  pospropd  18208  isnsg  18948  nsgbi  18950  elnmz  18956  nmzbi  18957  oddvdsnn0  19317  odeq  19323  odmulg  19329  isslw  19381  slwispgp  19384  gsumval3lem2  19674  gsumcom2  19743  abveq0  20270  cnt0  22681  kqfvima  23065  kqt0lem  23071  isr0  23072  r0cld  23073  regr1lem2  23075  nrmr0reg  23084  isfildlem  23192  cnextfvval  23400  xmeteq0  23675  imasf1oxmet  23712  comet  23853  dscmet  23912  nrmmetd  23914  tngngp  24002  tngngp3  24004  mbfsup  25012  mbfinf  25013  degltlem1  25421  logltb  25939  cxple2  26036  rlimcnp  26299  rlimcnp2  26300  isppw2  26448  sqf11  26472  slerec  27142  tgjustc1  27303  tgjustc2  27304  f1otrgitv  27698  nbuhgr2vtx1edgb  28186  dfconngr1  29018  eupth2lem3lem6  29063  nmlno0i  29622  nmlno0  29623  blocn  29635  ubth  29701  hvsubeq0  29896  hvaddcan  29898  hvsubadd  29905  normsub0  29964  hlim2  30020  pjoc1  30262  pjoc2  30267  chne0  30322  chsscon3  30328  chlejb1  30340  chnle  30342  h1de2ci  30384  elspansn  30394  elspansn2  30395  cmbr3  30436  cmcm  30442  cmcm3  30443  pjch1  30498  pjch  30522  pj11  30542  pjnel  30554  eigorth  30666  elnlfn  30756  nmlnop0  30826  lnopeq  30837  lnopcon  30863  lnfncon  30884  pjdifnormi  30995  chrelat2  31198  cvexch  31202  mdsym  31240  fmptcof2  31459  mgcoval  31729  mgcval  31730  mgccole1  31733  mgccole2  31734  mgcmnt1  31735  mgcmnt2  31736  mgccnv  31742  ist0cld  32283  zarclssn  32323  zart0  32329  signswch  33042  fnrelpredd  33562  cvmlift2lem12  33777  cvmlift2lem13  33778  satfv1lem  33825  satf0op  33840  fmlafvel  33848  abs2sqle  34137  abs2sqlt  34138  axextdist  34244  brimageg  34479  brdomaing  34487  brrangeg  34488  elhf2  34727  nn0prpwlem  34761  nn0prpw  34762  onsuct0  34880  bj-sbceqgALT  35336  bj-elabd2ALT  35362  bj-ru0  35380  eleq2w2ALT  35485  dfgcd3  35762  cbveud  35810  wl-3xorbi123d  35913  matunitlindf  36043  prdsbnd2  36221  isdrngo1  36382  eqrelf  36682  elsymrels5  36985  dfdisjs5  37141  eldisjs5  37155  mpets2  37270  pets  37281  lsatcmp  37432  llnexchb2  38299  lautset  38512  lautle  38514  sticksstones2  40522  dvdsexpnn0  40765  zindbi  41208  wepwsolem  41307  aomclem8  41326  onsupmaxb  41511  oaordnr  41568  omnord1  41577  oenord1  41588  ntrneik13  42312  ntrneix13  42313  ntrneik4w  42314  2sbc6g  42637  2sbc5g  42638  wessf1ornlem  43339  fourierdlem31  44311  fourierdlem42  44322  fourierdlem54  44333  funressndmafv2rn  45387  dfatbrafv2b  45409  fnbrafv2b  45412  ichbidv  45577  ichnfim  45588  sprsymrelf  45619  sprsymrelfo  45621  isomuspgrlem2b  45953  isomuspgrlem2d  45955  line2ylem  46769  line2xlem  46771  mofeu  46846  catprslem  46962
  Copyright terms: Public domain W3C validator