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  3650  elpwb  4571  ssdifsn  4752  brab2a  5732  elon2  6343  elovmpo  7634  eqop2  8011  iscard  9928  iscard2  9929  elnnnn0  12485  elfzo2  13623  bitsval  16394  1nprm  16649  funcpropd  17864  isfull  17874  isfth  17878  ismgmhm  18623  ismhm  18712  isghm  19147  isghmOLD  19148  ghmpropd  19188  isga  19223  oppgcntz  19296  gexdvdsi  19513  isrnghm  20350  isrhm  20387  issdrg  20697  abvpropd  20744  islmhm  20934  dfprm2  21383  prmirred  21384  elocv  21577  isobs  21629  iscn2  23125  iscnp2  23126  islocfin  23404  elflim2  23851  isfcls  23896  isnghm  24611  isnmhm  24634  0plef  25573  elply  26100  dchrelbas4  27154  brsslt  27697  nb3grpr  29309  ispligb  30406  isph  30751  abfmpunirn  32576  iscvm  35246  sscoid  35901  bj-pwvrelb  36886  bj-elsnb  37049  bj-ideqb  37147  bj-opelidb1ALT  37154  bj-elid5  37157  eldiophb  42745  eldioph3b  42753  eldioph4b  42799  bropabg  43312  brfvrcld2  43681  islmd  49654  iscmd  49655