Theorem biadan2 674

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 665	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))
3		biadan2.2	. . 3 ⊢ (𝜓 → (𝜑 ↔ 𝜒))
4	3	pm5.32i 669	. 2 ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜓 ∧ 𝜒))
5	2, 4	bitri 264	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 386

This theorem is referenced by:  elab4g  3355  elpwb  4169  brab2a  5194  elon2  5734  elovmpt2  6879  eqop2  7209  iscard  8801  iscard2  8802  elnnnn0  11336  elfzo2  12473  bitsval  15146  1nprm  15392  funcpropd  16560  isfull  16570  isfth  16574  ismhm  17337  isghm  17660  ghmpropd  17698  isga  17724  oppgcntz  17794  gexdvdsi  17998  isrhm  18721  abvpropd  18842  islmhm  19027  dfprm2  19842  prmirred  19843  elocv  20012  isobs  20064  iscn2  21042  iscnp2  21043  islocfin  21320  elflim2  21768  isfcls  21813  isnghm  22527  isnmhm  22550  0plef  23439  elply  23951  dchrelbas4  24968  nb3grpr  26284  ispligb  27329  isph  27677  abfmpunirn  29452  iscvm  31241  brsslt  31900  sscoid  32020  bj-ismoorec  33060  eldiophb  37320  eldioph3b  37328  eldioph4b  37375  issdrg  37767  brfvrcld2  37984  ismgmhm  41783  isrnghm  41892