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

Theorem 3anbi12d 1429
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 1428 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜂)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  w3a 1080
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 1082
This theorem is referenced by:  3anbi1d  1432  3anbi2d  1433  f1dom3el3dif  6892  fseq1m1p1  12832  dfrtrcl2  14255  imasdsval  16617  iscatd2  16781  ispos  17386  psgnunilem1  18352  ringpropd  19022  mdetunilem3  20907  mdetunilem9  20913  dvfsumlem2  24307  istrkge  25925  axtg5seg  25933  axtgeucl  25940  iscgrad  26279  axlowdim  26430  axeuclid  26432  eengtrkge  26456  umgrvad2edg  26678  upgr3v3e3cycl  27646  upgr4cycl4dv4e  27651  lt2addrd  30163  xlt2addrd  30170  sigaval  30987  issgon  30999  brafs  31560  loop1cycl  31992  etasslt  32883  brofs  33075  funtransport  33101  fvtransport  33102  brifs  33113  ifscgr  33114  brcgr3  33116  cgr3permute3  33117  brfs  33149  btwnconn1lem11  33167  funray  33210  fvray  33211  funline  33212  fvline  33214  lpolsetN  38149  rmydioph  39096  iunrelexpmin2  39542  ichexmpl1  43113
  Copyright terms: Public domain W3C validator