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

Theorem 3anbi1i 1245
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 249 . 2 (𝜒𝜒)
3 biid 249 . 2 (𝜃𝜃)
41, 2, 33anbi123i 1243 1 ((𝜑𝜒𝜃) ↔ (𝜓𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wb 194  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  iinfi  8179  fzolb  12296  brfi1uzind  13077  opfi1uzind  13080  brfi1uzindOLD  13083  opfi1uzindOLD  13086  sqrlem5  13777  bitsmod  14938  isfunc  16289  txcn  21177  trfil2  21439  isclmp  22632  eulerpartlemn  29572  bnj976  29904  bnj543  30019  bnj594  30038  bnj917  30060  topdifinffinlem  32170  dath  33839  elfzolborelfzop1  42101  nnolog2flm1  42180
  Copyright terms: Public domain W3C validator