Theorem biadanii 834

Description: Inference associated with biadani 832. 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 832	. 2 ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒)))
4	1, 3	mpbi 233	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  elab4g  3640  elpwb  4568  ssdifsn  4751  brab2a  5749  cnveq0b  6198  elon2  6380  elovmpo  7676  eqop2  8054  iscard  10069  iscard2  10070  elnnnn0  12662  elfzo2  13809  bitsval  16609  1nprm  16869  funcpropd  18092  isfull  18102  isfth  18106  ismgmhm  18900  ismhm  18995  isghm  19445  ghmpropd  19485  isga  19520  oppgcntz  19593  gexdvdsi  19812  isrnghm  20686  isrhm  20724  issdrg  21060  abvpropd  21107  islmhm  21317  dfprm2  21794  prmirred  21795  elocv  21989  isobs  22041  iscn2  23571  iscnp2  23572  islocfin  23851  elflim2  24298  isfcls  24343  isnghm  25057  isnmhm  25080  0plef  26008  elply  26528  dchrelbas4  27585  brslts  28163  nb3grpr  29978  ispligb  31094  isph  31439  abfmpunirn  33303  iscvm  36148  sscoid  36805  bj-pwvrelb  37940  bj-elsnb  38118  bj-ideqb  38223  bj-opelidb1ALT  38230  bj-elid5  38233  eldiophb  43911  eldioph3b  43919  eldioph4b  43961  bropabg  44468  brfvrcld2  44835  islmd  50990  iscmd  50991