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

Theorem 3anbi3i 1199
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
3anbi3i ((𝜒𝜃𝜑) ↔ (𝜒𝜃𝜓))

Proof of Theorem 3anbi3i
StepHypRef Expression
1 biid 253 . 2 (𝜒𝜒)
2 biid 253 . 2 (𝜃𝜃)
3 3anbi1i.1 . 2 (𝜑𝜓)
41, 2, 33anbi123i 1195 1 ((𝜒𝜃𝜑) ↔ (𝜒𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 198  w3a 1108
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 199  df-an 386  df-3an 1110
This theorem is referenced by:  cadcomb  1723  dfer2  7983  axgroth2  9935  oppgsubm  18104  xrsdsreclb  20115  ordthaus  21517  qtopeu  21848  regr1lem2  21872  isfbas2  21967  isclmp  23224  umgr2edg1  26444  xrge0adddir  30208  isros  30747  bnj964  31530  bnj1033  31554  dfon2lem7  32206  outsideofcom  32748  linecom  32770  linerflx2  32771  topdifinffinlem  33693  rdgeqoa  33716  ishlat2  35374  lhpex2leN  36034  lmbr3v  40721  lmbr3  40723  fourierdlem103  41169  fourierdlem104  41170  issmf  41683  issmff  41689  issmfle  41700  issmfgt  41711  issmfge  41724
  Copyright terms: Public domain W3C validator