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

Theorem 3anbi12d 1428
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 263 . 2 (𝜑 → (𝜂𝜂))
41, 2, 33anbi123d 1427 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜂)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  3anbi1d  1431  3anbi2d  1432  f1dom3el3dif  7018  fseq1m1p1  12970  dfrtrcl2  14409  imasdsval  16776  iscatd2  16940  ispos  17545  psgnunilem1  18550  ringpropd  19261  mdetunilem3  21151  mdetunilem9  21157  dvfsumlem2  24551  istrkge  26170  axtg5seg  26178  axtgeucl  26185  iscgrad  26524  axlowdim  26674  axeuclid  26676  eengtrkge  26700  umgrvad2edg  26922  upgr3v3e3cycl  27886  upgr4cycl4dv4e  27891  lt2addrd  30401  xlt2addrd  30408  sigaval  31269  issgon  31281  brafs  31842  loop1cycl  32281  etasslt  33171  brofs  33363  funtransport  33389  fvtransport  33390  brifs  33401  ifscgr  33402  brcgr3  33404  cgr3permute3  33405  brfs  33437  btwnconn1lem11  33455  funray  33498  fvray  33499  funline  33500  fvline  33502  lpolsetN  38498  rmydioph  39489  iunrelexpmin2  39935  fundcmpsurinj  43446  ichexmpl1  43508
  Copyright terms: Public domain W3C validator