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

Theorem 3anbi12d 1433
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 1432 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜂)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  w3a 1084
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  df-an 396  df-3an 1086
This theorem is referenced by:  3anbi1d  1436  3anbi2d  1437  f1dom3el3dif  7260  xpord2pred  8125  fseq1m1p1  13573  dfrtrcl2  15006  imasdsval  17460  iscatd2  17624  ispos  18269  psgnunilem1  19403  rngpropd  20069  ringpropd  20177  mdetunilem3  22438  mdetunilem9  22444  dvfsumlem2  25883  dvfsumlem2OLD  25884  istrkge  28177  axtg5seg  28185  axtgeucl  28192  iscgrad  28531  axlowdim  28688  axeuclid  28690  eengtrkge  28714  umgrvad2edg  28939  upgr3v3e3cycl  29902  upgr4cycl4dv4e  29907  lt2addrd  32433  xlt2addrd  32440  sigaval  33598  issgon  33610  brafs  34173  loop1cycl  34617  brofs  35472  funtransport  35498  fvtransport  35499  brifs  35510  ifscgr  35511  brcgr3  35513  cgr3permute3  35514  brfs  35546  btwnconn1lem11  35564  funray  35607  fvray  35608  funline  35609  fvline  35611  lpolsetN  40843  rmydioph  42242  tfsconcatrev  42587  iunrelexpmin2  42952  fundcmpsurinj  46562  ichexmpl1  46622  iscnrm3r  47769  iscnrm3l  47772
  Copyright terms: Public domain W3C validator