Theorem biadan2 672

Description: Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.)

Hypotheses

Ref	Expression
biadan2.1	⊢ (𝜑 → 𝜓)
biadan2.2	⊢ (𝜓 → (𝜑 ↔ 𝜒))

Assertion

Ref	Expression
biadan2	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Proof of Theorem biadan2

Step	Hyp	Ref	Expression
1		biadan2.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	pm4.71ri 663	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))
3		biadan2.2	. . 3 ⊢ (𝜓 → (𝜑 ↔ 𝜒))
4	3	pm5.32i 667	. 2 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜓 ∧ 𝜒))
5	2, 4	bitri 263	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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

This theorem is referenced by:  elab4g  3324  brab2a  5091  brab2ga  5117  elon2  5651  elovmpt2  6777  eqop2  7100  iscard  8684  iscard2  8685  elnnnn0  11213  elfzo2  12342  bitsval  14984  1nprm  15230  funcpropd  16383  isfull  16393  isfth  16397  ismhm  17160  isghm  17483  ghmpropd  17521  isga  17547  oppgcntz  17617  gexdvdsi  17821  isrhm  18544  abvpropd  18665  islmhm  18848  dfprm2  19661  prmirred  19662  elocv  19831  isobs  19883  iscn2  20852  iscnp2  20853  islocfin  21130  elflim2  21578  isfcls  21623  isnghm  22337  isnmhm  22360  0plef  23245  elply  23755  dchrelbas4  24768  nb3grapr  25982  isph  27061  abfmpunirn  28832  iscvm  30495  sscoid  31190  eldiophb  36338  eldioph3b  36346  eldioph4b  36393  issdrg  36786  brfvrcld2  37003  nb3grpr  40610  ismgmhm  41573  isrnghm  41682