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

Theorem 3anbi1i 1414
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 251 . 2 (𝜒𝜒)
3 biid 251 . 2 (𝜃𝜃)
41, 2, 33anbi123i 1412 1 ((𝜑𝜒𝜃) ↔ (𝜓𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wb 196  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  iinfi  8476  fzolb  12641  brfi1uzind  13443  opfi1uzind  13446  sqrlem5  14157  bitsmod  15331  isfunc  16696  txcn  21602  trfil2  21863  isclmp  23068  eulerpartlemn  30723  bnj976  31126  bnj543  31241  bnj594  31260  bnj917  31282  topdifinffinlem  33477  dath  35494  elfzolborelfzop1  42788  nnolog2flm1  42863
  Copyright terms: Public domain W3C validator