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

Theorem 3anbi3i 1248
 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 250 . 2 (𝜒𝜒)
2 biid 250 . 2 (𝜃𝜃)
3 3anbi1i.1 . 2 (𝜑𝜓)
41, 2, 33anbi123i 1244 1 ((𝜒𝜃𝜑) ↔ (𝜒𝜃𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  cadcomb  1543  dfer2  7630  axgroth2  9526  oppgsubm  17615  xrsdsreclb  19612  ordthaus  20998  qtopeu  21329  regr1lem2  21353  isfbas2  21449  isclmp  22705  nbgrasym  25968  xrge0adddir  29023  isros  29558  bnj964  30267  bnj1033  30291  dfon2lem7  30938  outsideofcom  31405  linecom  31427  linerflx2  31428  topdifinffinlem  32371  rdgeqoa  32394  ishlat2  33658  lhpex2leN  34317  fourierdlem103  39102  fourierdlem104  39103  issmf  39614  issmff  39620  issmfle  39632  issmfgt  39643  issmfge  39656  umgr2edg1  40438
 Copyright terms: Public domain W3C validator