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  3636  elpwb  4560  ssdifsn  4742  brab2a  5715  elon2  6326  elovmpo  7601  eqop2  7974  iscard  9885  iscard2  9886  elnnnn0  12442  elfzo2  13576  bitsval  16349  1nprm  16604  funcpropd  17824  isfull  17834  isfth  17838  ismgmhm  18619  ismhm  18708  isghm  19142  isghmOLD  19143  ghmpropd  19183  isga  19218  oppgcntz  19291  gexdvdsi  19510  isrnghm  20375  isrhm  20412  issdrg  20719  abvpropd  20766  islmhm  20977  dfprm2  21426  prmirred  21427  elocv  21621  isobs  21673  iscn2  23180  iscnp2  23181  islocfin  23459  elflim2  23906  isfcls  23951  isnghm  24665  isnmhm  24688  0plef  25627  elply  26154  dchrelbas4  27208  brsslt  27752  nb3grpr  29404  ispligb  30501  isph  30846  abfmpunirn  32679  iscvm  35402  sscoid  36054  bj-pwvrelb  37042  bj-elsnb  37205  bj-ideqb  37303  bj-opelidb1ALT  37310  bj-elid5  37313  eldiophb  42941  eldioph3b  42949  eldioph4b  42995  bropabg  43507  brfvrcld2  43875  islmd  49852  iscmd  49853