Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  3anbi3d GIF version

Theorem 3anbi3d 1297
 Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
Hypothesis
Ref Expression
3anbi1d.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
3anbi3d (𝜑 → ((𝜃𝜏𝜓) ↔ (𝜃𝜏𝜒)))

Proof of Theorem 3anbi3d
StepHypRef Expression
1 biidd 171 . 2 (𝜑 → (𝜃𝜃))
2 3anbi1d.1 . 2 (𝜑 → (𝜓𝜒))
31, 23anbi13d 1293 1 (𝜑 → ((𝜃𝜏𝜓) ↔ (𝜃𝜏𝜒)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104   ∧ w3a 963 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116  df-3an 965 This theorem is referenced by:  ceqsex3v  2731  ceqsex4v  2732  ceqsex8v  2734  vtocl3gaf  2758  mob  2869  ordsoexmid  4484  tfr1onlemaccex  6252  tfrcllemaccex  6265  fseq1m1p1  9905  summodc  11183  fsum3  11187  divalglemnn  11649  divalglemeunn  11652  divalglemex  11653  divalglemeuneg  11654
 Copyright terms: Public domain W3C validator