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

Theorem 3anbi3i 1163
 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 251 . 2 (𝜒𝜒)
2 biid 251 . 2 (𝜃𝜃)
3 3anbi1i.1 . 2 (𝜑𝜓)
41, 2, 33anbi123i 1159 1 ((𝜒𝜃𝜑) ↔ (𝜒𝜃𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ w3a 1072 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 385  df-3an 1074 This theorem is referenced by:  cadcomb  1699  dfer2  7910  axgroth2  9837  oppgsubm  17990  xrsdsreclb  19993  ordthaus  21388  qtopeu  21719  regr1lem2  21743  isfbas2  21838  isclmp  23095  umgr2edg1  26300  xrge0adddir  29999  isros  30538  bnj964  31318  bnj1033  31342  dfon2lem7  31997  outsideofcom  32539  linecom  32561  linerflx2  32562  topdifinffinlem  33504  rdgeqoa  33527  ishlat2  35141  lhpex2leN  35800  lmbr3v  40478  lmbr3  40480  fourierdlem103  40927  fourierdlem104  40928  issmf  41441  issmff  41447  issmfle  41458  issmfgt  41469  issmfge  41482
 Copyright terms: Public domain W3C validator