Theorem biadanii 818

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  elab4g  3607  elpwb  4540  ssdifsn  4718  brab2a  5670  elon2  6262  elovmpo  7492  eqop2  7847  iscard  9664  iscard2  9665  elnnnn0  12206  elfzo2  13319  bitsval  16059  1nprm  16312  funcpropd  17532  isfull  17542  isfth  17546  ismhm  18347  isghm  18749  ghmpropd  18787  isga  18812  oppgcntz  18886  gexdvdsi  19103  isrhm  19880  issdrg  19978  abvpropd  20017  islmhm  20204  dfprm2  20607  prmirred  20608  elocv  20785  isobs  20837  iscn2  22297  iscnp2  22298  islocfin  22576  elflim2  23023  isfcls  23068  isnghm  23793  isnmhm  23816  0plef  24741  elply  25261  dchrelbas4  26296  nb3grpr  27652  ispligb  28740  isph  29085  abfmpunirn  30891  iscvm  33121  brsslt  33907  sscoid  34142  bj-pwvrelb  35010  bj-elsnb  35159  bj-ideqb  35257  bj-opelidb1ALT  35264  bj-elid5  35267  eldiophb  40495  eldioph3b  40503  eldioph4b  40549  brfvrcld2  41189  ismgmhm  45225  isrnghm  45338