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

Theorem bibi12d 336
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 334 . 2 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
3 imbi12d.2 . . 3 (𝜑 → (𝜃𝜏))
43bibi2d 333 . 2 (𝜑 → ((𝜒𝜃) ↔ (𝜒𝜏)))
52, 4bitrd 270 1 (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  bi2bian9  624  xorbi12d  1632  sb8eu  2677  cleqh  2919  vtoclb  3467  vtoclbg  3471  ceqsexg  3539  elabgf  3554  reu6  3604  ru  3643  sbcbig  3689  unineq  4090  sbcnestgf  4203  preq12bg  4584  prel12gOLD  4585  axrep1  4978  axrep4  4982  nalset  5003  opthg  5148  opelopabsb  5193  isso2i  5277  opeliunxp2  5476  resieq  5625  elimasng  5715  cbviota  6079  iota2df  6098  fnbrfvb  6466  fvelimab  6484  fvopab5  6541  fmptco  6629  fsng  6637  fsn2g  6638  fressnfv  6661  fnpr2g  6709  isorel  6810  isocnv  6814  isocnv3  6816  isotr  6820  ovg  7039  caovcang  7075  caovordg  7081  caovord3d  7084  caovord  7085  orduninsuc  7283  opeliunxp2f  7581  brtpos  7606  dftpos4  7616  omopth  7985  ecopovsym  8095  xpf1o  8371  nneneq  8392  r1pwALT  8966  karden  9015  infxpenlem  9129  aceq0  9234  cflim2  9380  zfac  9577  ttukeylem1  9626  axextnd  9708  axrepndlem1  9709  axrepndlem2  9710  axrepnd  9711  axacndlem5  9728  zfcndrep  9731  zfcndac  9736  winalim  9812  gruina  9935  ltrnq  10096  ltsosr  10210  ltasr  10216  axpre-lttri  10281  axpre-ltadd  10283  nn0sub  11629  zextle  11736  zextlt  11737  xlesubadd  12331  sqeqor  13221  nn0opth2  13299  rexfiuz  14330  climshft  14550  rpnnen2lem10  15192  dvdsext  15286  ltoddhalfle  15325  halfleoddlt  15326  sumodd  15351  sadcadd  15419  dvdssq  15519  rpexp  15669  pcdvdsb  15810  imasleval  16426  isacs2  16538  acsfiel  16539  funcres2b  16781  pospropd  17359  isnsg  17845  nsgbi  17847  elnmz  17855  nmzbi  17856  oddvdsnn0  18184  odeq  18190  odmulg  18194  isslw  18244  slwispgp  18247  gsumval3lem2  18528  gsumcom2  18595  abveq0  19050  cnt0  21385  kqfvima  21768  kqt0lem  21774  isr0  21775  r0cld  21776  regr1lem2  21778  nrmr0reg  21787  isfildlem  21895  cnextfvval  22103  xmeteq0  22377  imasf1oxmet  22414  comet  22552  dscmet  22611  nrmmetd  22613  tngngp  22692  tngngp3  22694  mbfsup  23668  mbfinf  23669  degltlem1  24069  logltb  24583  cxple2  24680  rlimcnp  24929  rlimcnp2  24930  isppw2  25078  sqf11  25102  f1otrgitv  25987  nbuhgr2vtx1edgb  26487  dfconngr1  27384  eupth2lem3lem6  27429  nmlno0i  28000  nmlno0  28001  blocn  28013  ubth  28080  hvsubeq0  28276  hvaddcan  28278  hvsubadd  28285  normsub0  28344  hlim2  28400  pjoc1  28644  pjoc2  28649  chne0  28704  chsscon3  28710  chlejb1  28722  chnle  28724  h1de2ci  28766  elspansn  28776  elspansn2  28777  cmbr3  28818  cmcm  28824  cmcm3  28825  pjch1  28880  pjch  28904  pj11  28924  pjnel  28936  eigorth  29048  elnlfn  29138  nmlnop0  29208  lnopeq  29219  lnopcon  29245  lnfncon  29266  pjdifnormi  29377  chrelat2  29580  cvexch  29584  mdsym  29622  fmptcof2  29807  signswch  30986  cvmlift2lem12  31641  cvmlift2lem13  31642  abs2sqle  31918  abs2sqlt  31919  dfpo2  31989  eqfunresadj  32003  br1steqgOLD  32016  br2ndeqgOLD  32017  axextdist  32047  slerec  32266  brimageg  32377  brdomaing  32385  brrangeg  32386  elhf2  32625  nn0prpwlem  32660  nn0prpw  32661  onsuct0  32779  bj-abbi  33108  bj-axrep1  33121  bj-axrep4  33124  bj-nalset  33127  bj-sbceqgALT  33224  bj-ru0  33262  dfgcd3  33506  matunitlindf  33739  prdsbnd2  33924  isdrngo1  34085  eqrelf  34357  elsymrels5  34634  lsatcmp  34802  llnexchb2  35668  lautset  35881  lautle  35883  zindbi  38030  wepwsolem  38131  aomclem8  38150  ntrneik13  38914  ntrneix13  38915  ntrneik4w  38916  2sbc6g  39133  2sbc5g  39134  wessf1ornlem  39878  fourierdlem31  40852  fourierdlem42  40863  fourierdlem54  40874  funressndmafv2rn  41830  dfatbrafv2b  41852  fnbrafv2b  41855  sprsymrelf  42331  sprsymrelfo  42333
  Copyright terms: Public domain W3C validator