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

Theorem 3anbi1i 1151
 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 262 . 2 (𝜒𝜒)
3 biid 262 . 2 (𝜃𝜃)
41, 2, 33anbi123i 1149 1 ((𝜑𝜒𝜃) ↔ (𝜓𝜒𝜃))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207   ∧ w3a 1081 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 1083 This theorem is referenced by:  iinfi  8873  fzolb  13037  brfi1uzind  13849  opfi1uzind  13852  sqrlem5  14599  bitsmod  15777  isfunc  17126  txcn  22152  trfil2  22413  isclmp  23618  eulerpartlemn  31527  bnj976  31937  bnj543  32053  bnj594  32072  bnj917  32094  topdifinffinlem  34499  dath  36741  ichexmpl1  43465  elfzolborelfzop1  44408  nnolog2flm1  44484
 Copyright terms: Public domain W3C validator