Theorem biadanii 857

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  elab4g  3576  elpwb  4391  ssdifsn  4539  brab2a  5433  elon2  5978  elovmpt2  7144  eqop2  7476  iscard  9121  iscard2  9122  elnnnn0  11670  elfzo2  12775  bitsval  15526  1nprm  15771  funcpropd  16919  isfull  16929  isfth  16933  ismhm  17697  isghm  18018  ghmpropd  18056  isga  18081  oppgcntz  18151  gexdvdsi  18356  isrhm  19084  abvpropd  19205  islmhm  19393  dfprm2  20209  prmirred  20210  elocv  20382  isobs  20434  iscn2  21420  iscnp2  21421  islocfin  21698  elflim2  22145  isfcls  22190  isnghm  22904  isnmhm  22927  0plef  23845  elply  24357  dchrelbas4  25388  nb3grpr  26687  ispligb  27883  isph  28228  abfmpunirn  29997  iscvm  31783  brsslt  32434  sscoid  32554  bj-ismoorec  33578  eldiophb  38159  eldioph3b  38167  eldioph4b  38214  issdrg  38605  brfvrcld2  38820  ismgmhm  42644  isrnghm  42753