Theorem biadanii 822

Description: Inference associated with biadani 820. Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) (Proof shortened by BJ, 4-Mar-2023.)

Hypotheses

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

Assertion

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

Proof of Theorem biadanii

Step	Hyp	Ref	Expression
1		biadanii.2	. 2 ⊢ (𝜓 → (𝜑 ↔ 𝜒))
2		biadani.1	. . 3 ⊢ (𝜑 → 𝜓)
3	2	biadani 820	. 2 ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒)))
4	1, 3	mpbi 230	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  elab4g  3685  elpwb  4612  ssdifsn  4792  brab2a  5781  elon2  6396  elovmpo  7677  eqop2  8055  iscard  10012  iscard2  10013  elnnnn0  12566  elfzo2  13698  bitsval  16457  1nprm  16712  funcpropd  17953  isfull  17963  isfth  17967  ismgmhm  18721  ismhm  18810  isghm  19245  isghmOLD  19246  ghmpropd  19286  isga  19321  oppgcntz  19397  gexdvdsi  19615  isrnghm  20457  isrhm  20494  issdrg  20805  abvpropd  20852  islmhm  21043  dfprm2  21501  prmirred  21502  elocv  21703  isobs  21757  iscn2  23261  iscnp2  23262  islocfin  23540  elflim2  23987  isfcls  24032  isnghm  24759  isnmhm  24782  0plef  25720  elply  26248  dchrelbas4  27301  brsslt  27844  nb3grpr  29413  ispligb  30505  isph  30850  abfmpunirn  32668  iscvm  35243  sscoid  35894  bj-pwvrelb  36880  bj-elsnb  37043  bj-ideqb  37141  bj-opelidb1ALT  37148  bj-elid5  37151  eldiophb  42744  eldioph3b  42752  eldioph4b  42798  bropabg  43312  brfvrcld2  43681