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  3627  elpwb  4550  ssdifsn  4732  brab2a  5718  elon2  6329  elovmpo  7606  eqop2  7979  iscard  9893  iscard2  9894  elnnnn0  12474  elfzo2  13610  bitsval  16387  1nprm  16642  funcpropd  17863  isfull  17873  isfth  17877  ismgmhm  18658  ismhm  18747  isghm  19184  isghmOLD  19185  ghmpropd  19225  isga  19260  oppgcntz  19333  gexdvdsi  19552  isrnghm  20415  isrhm  20452  issdrg  20759  abvpropd  20806  islmhm  21017  dfprm2  21466  prmirred  21467  elocv  21661  isobs  21713  iscn2  23216  iscnp2  23217  islocfin  23495  elflim2  23942  isfcls  23987  isnghm  24701  isnmhm  24724  0plef  25652  elply  26173  dchrelbas4  27223  brslts  27771  nb3grpr  29468  ispligb  30566  isph  30911  abfmpunirn  32743  iscvm  35460  sscoid  36112  bj-pwvrelb  37224  bj-elsnb  37387  bj-ideqb  37492  bj-opelidb1ALT  37499  bj-elid5  37502  eldiophb  43206  eldioph3b  43214  eldioph4b  43260  bropabg  43772  brfvrcld2  44140  islmd  50155  iscmd  50156