Theorem biadanii 821

Description: Inference associated with biadani 819. 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 819	. 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  3638  elpwb  4562  ssdifsn  4744  brab2a  5717  elon2  6328  elovmpo  7603  eqop2  7976  iscard  9887  iscard2  9888  elnnnn0  12444  elfzo2  13578  bitsval  16351  1nprm  16606  funcpropd  17826  isfull  17836  isfth  17840  ismgmhm  18621  ismhm  18710  isghm  19144  isghmOLD  19145  ghmpropd  19185  isga  19220  oppgcntz  19293  gexdvdsi  19512  isrnghm  20377  isrhm  20414  issdrg  20721  abvpropd  20768  islmhm  20979  dfprm2  21428  prmirred  21429  elocv  21623  isobs  21675  iscn2  23182  iscnp2  23183  islocfin  23461  elflim2  23908  isfcls  23953  isnghm  24667  isnmhm  24690  0plef  25629  elply  26156  dchrelbas4  27210  brslts  27758  nb3grpr  29455  ispligb  30552  isph  30897  abfmpunirn  32730  iscvm  35453  sscoid  36105  bj-pwvrelb  37099  bj-elsnb  37262  bj-ideqb  37364  bj-opelidb1ALT  37371  bj-elid5  37374  eldiophb  43009  eldioph3b  43017  eldioph4b  43063  bropabg  43575  brfvrcld2  43943  islmd  49920  iscmd  49921