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

Theorem 3anbi12d 1554
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 253 . 2 (𝜑 → (𝜂𝜂))
41, 2, 33anbi123d 1553 1 (𝜑 → ((𝜓𝜃𝜂) ↔ (𝜒𝜏𝜂)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  w3a 1100
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  df-an 385  df-3an 1102
This theorem is referenced by:  3anbi1d  1557  3anbi2d  1558  f1dom3el3dif  6748  fseq1m1p1  12636  dfrtrcl2  14023  imasdsval  16378  iscatd2  16544  ispos  17150  psgnunilem1  18112  ringpropd  18782  mdetunilem3  20629  mdetunilem9  20635  dvfsumlem2  24002  istrkge  25568  axtg5seg  25576  axtgeucl  25583  iscgrad  25915  axlowdim  26053  axeuclid  26055  eengtrkge  26078  umgrvad2edg  26318  upgr3v3e3cycl  27351  upgr4cycl4dv4e  27356  lt2addrd  29841  xlt2addrd  29848  sigaval  30496  issgon  30509  brafs  31073  etasslt  32239  brofs  32431  funtransport  32457  fvtransport  32458  brifs  32469  ifscgr  32470  brcgr3  32472  cgr3permute3  32473  brfs  32505  btwnconn1lem11  32523  funray  32566  fvray  32567  funline  32568  fvline  32570  lpolsetN  37261  rmydioph  38080  iunrelexpmin2  38502
  Copyright terms: Public domain W3C validator