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

Theorem 3anbi3i 1247
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 249 . 2 (𝜒𝜒)
2 biid 249 . 2 (𝜃𝜃)
3 3anbi1i.1 . 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:  cadcomb  1542  dfer2  7607  axgroth2  9503  oppgsubm  17563  xrsdsreclb  19560  ordthaus  20945  qtopeu  21276  regr1lem2  21300  isfbas2  21396  isclmp  22652  nbgrasym  25761  xrge0adddir  28816  isros  29351  bnj964  30060  bnj1033  30084  dfon2lem7  30731  outsideofcom  31198  linecom  31220  linerflx2  31221  topdifinffinlem  32154  rdgeqoa  32177  ishlat2  33441  lhpex2leN  34100  fourierdlem103  38885  fourierdlem104  38886  issmf  39397  issmff  39403  issmfle  39415  issmfgt  39426  issmfge  39439  umgr2edg1  40419
  Copyright terms: Public domain W3C validator