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

Theorem 3anbi1i 1252
 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 1250 1 ((𝜑𝜒𝜃) ↔ (𝜓𝜒𝜃))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ w3a 1037 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 386  df-3an 1039 This theorem is referenced by:  iinfi  8320  fzolb  12472  brfi1uzind  13275  opfi1uzind  13278  brfi1uzindOLD  13281  opfi1uzindOLD  13284  sqrlem5  13981  bitsmod  15152  isfunc  16518  txcn  21423  trfil2  21685  isclmp  22891  eulerpartlemn  30428  bnj976  30833  bnj543  30948  bnj594  30967  bnj917  30989  topdifinffinlem  33175  dath  34848  elfzolborelfzop1  42080  nnolog2flm1  42155
 Copyright terms: Public domain W3C validator