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

Theorem 3anbi3i 1160
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 261 . 2 (𝜒𝜒)
2 biid 261 . 2 (𝜃𝜃)
3 3anbi1i.1 . 2 (𝜑𝜓)
41, 2, 33anbi123i 1156 1 ((𝜒𝜃𝜑) ↔ (𝜒𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  cadcomb  1615  dfwrecsOLD  8248  dfer2  8655  ttrclresv  9661  axgroth2  10769  oppgsubm  19151  xrsdsreclb  20867  ordthaus  22758  qtopeu  23090  regr1lem2  23114  isfbas2  23209  isclmp  24483  umgr2edg1  28208  xrge0adddir  31939  isros  32831  bnj964  33619  bnj1033  33645  cusgr3cyclex  33794  dfon2lem7  34427  outsideofcom  34766  linecom  34788  linerflx2  34789  topdifinffinlem  35868  rdgeqoa  35891  ishlat2  37865  lhpex2leN  38526  lmbr3v  44076  lmbr3  44078  fourierdlem103  44540  fourierdlem104  44541  issmf  45059  issmff  45065  issmfle  45076  issmfgt  45087  issmfge  45101  funcf2lem  47128
  Copyright terms: Public domain W3C validator