Theorem biadanii 834

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  elab4g  3644  elpwb  4572  ssdifsn  4758  brab2a  5756  elon2  6375  elovmpo  7665  eqop2  8035  iscard  9977  iscard2  9978  elnnnn0  12564  elfzo2  13709  bitsval  16506  1nprm  16761  funcpropd  17983  isfull  17993  isfth  17997  ismgmhm  18788  ismhm  18882  isghm  19332  ghmpropd  19372  isga  19407  oppgcntz  19480  gexdvdsi  19699  isrnghm  20571  isrhm  20609  issdrg  20943  abvpropd  20990  islmhm  21200  dfprm2  21675  prmirred  21676  elocv  21870  isobs  21922  iscn2  23447  iscnp2  23448  islocfin  23727  elflim2  24174  isfcls  24219  isnghm  24933  isnmhm  24956  0plef  25884  elply  26405  dchrelbas4  27460  brslts  28008  nb3grpr  29792  ispligb  30902  isph  31247  abfmpunirn  33070  iscvm  35790  sscoid  36442  bj-pwvrelb  37592  bj-elsnb  37756  bj-ideqb  37862  bj-opelidb1ALT  37869  bj-elid5  37872  eldiophb  43548  eldioph3b  43556  eldioph4b  43598  bropabg  44110  brfvrcld2  44478  islmd  50502  iscmd  50503