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

Theorem 3anbi12d 1439
Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
Hypotheses
Ref Expression
3anbi12d.1 (𝜑 → (𝜓𝜒))
3anbi12d.2 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
3anbi12d (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜂)))

Proof of Theorem 3anbi12d
StepHypRef Expression
1 3anbi12d.1 . 2 (𝜑 → (𝜓𝜒))
2 3anbi12d.2 . 2 (𝜑 → (𝜃𝜏))
3 biidd 262 . 2 (𝜑 → (𝜂𝜂))
41, 2, 33anbi123d 1438 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜂)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  w3a 1087
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  df-an 396  df-3an 1089
This theorem is referenced by:  3anbi1d  1442  3anbi2d  1443  f1dom3el3dif  7289  xpord2pred  8170  fseq1m1p1  13639  dfrtrcl2  15101  imasdsval  17560  iscatd2  17724  ispos  18360  psgnunilem1  19511  rngpropd  20171  ringpropd  20285  mdetunilem3  22620  mdetunilem9  22626  dvfsumlem2  26067  dvfsumlem2OLD  26068  istrkge  28465  axtg5seg  28473  axtgeucl  28480  iscgrad  28819  axlowdim  28976  axeuclid  28978  eengtrkge  29002  umgrvad2edg  29230  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  lt2addrd  32755  xlt2addrd  32762  constrsuc  33779  constrconj  33786  sigaval  34112  issgon  34124  brafs  34687  loop1cycl  35142  brofs  36006  funtransport  36032  fvtransport  36033  brifs  36044  ifscgr  36045  brcgr3  36047  cgr3permute3  36048  brfs  36080  btwnconn1lem11  36098  funray  36141  fvray  36142  funline  36143  fvline  36145  lpolsetN  41484  rmydioph  43026  tfsconcatrev  43361  iunrelexpmin2  43725  fundcmpsurinj  47396  ichexmpl1  47456  cycl3grtri  47914  grimgrtri  47916  usgrgrtrirex  47917  isubgr3stgrlem4  47936  grlimgrtri  47963  iscnrm3r  48845  iscnrm3l  48848
  Copyright terms: Public domain W3C validator