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

Theorem 3anbi1i 1157
Description: Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
Hypothesis
Ref Expression
3anbi1i.1 (𝜑𝜓)
Assertion
Ref Expression
3anbi1i ((𝜑𝜒𝜃) ↔ (𝜓𝜒𝜃))

Proof of Theorem 3anbi1i
StepHypRef Expression
1 3anbi1i.1 . 2 (𝜑𝜓)
2 biid 261 . 2 (𝜒𝜒)
3 biid 261 . 2 (𝜃𝜃)
41, 2, 33anbi123i 1155 1 ((𝜑𝜒𝜃) ↔ (𝜓𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wb 206  w3a 1086
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 1088
This theorem is referenced by:  iinfi  9344  fzolb  13602  brfi1uzind  14449  opfi1uzind  14452  01sqrexlem5  15188  bitsmod  16382  isfunc  17802  txcn  23489  trfil2  23750  isclmp  24973  eulerpartlemn  34345  bnj976  34740  bnj543  34856  bnj594  34875  bnj917  34897  topdifinffinlem  37308  dath  39703  oeord2com  43273  ichexmpl1  47443  grtriproplem  47911  grtrif1o  47914  elfzolborelfzop1  48481  nnolog2flm1  48552  isthincd2  49399
  Copyright terms: Public domain W3C validator