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

Theorem 3anbi1i 1158
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 1156 1 ((𝜑𝜒𝜃) ↔ (𝜓𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wb 205  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  iinfi  9412  fzolb  13638  brfi1uzind  14459  opfi1uzind  14462  01sqrexlem5  15193  bitsmod  16377  isfunc  17814  txcn  23130  trfil2  23391  isclmp  24613  eulerpartlemn  33380  bnj976  33788  bnj543  33904  bnj594  33923  bnj917  33945  topdifinffinlem  36228  dath  38607  oeord2com  42061  ichexmpl1  46137  elfzolborelfzop1  47200  nnolog2flm1  47276  isthincd2  47658
  Copyright terms: Public domain W3C validator