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  3699  elpwb  4630  ssdifsn  4813  brab2a  5793  elon2  6406  elovmpo  7695  eqop2  8073  iscard  10044  iscard2  10045  elnnnn0  12596  elfzo2  13719  bitsval  16470  1nprm  16726  funcpropd  17967  isfull  17977  isfth  17981  ismgmhm  18734  ismhm  18820  isghm  19255  isghmOLD  19256  ghmpropd  19296  isga  19331  oppgcntz  19407  gexdvdsi  19625  isrnghm  20467  isrhm  20504  issdrg  20811  abvpropd  20858  islmhm  21049  dfprm2  21507  prmirred  21508  elocv  21709  isobs  21763  iscn2  23267  iscnp2  23268  islocfin  23546  elflim2  23993  isfcls  24038  isnghm  24765  isnmhm  24788  0plef  25726  elply  26254  dchrelbas4  27305  brsslt  27848  nb3grpr  29417  ispligb  30509  isph  30854  abfmpunirn  32670  iscvm  35227  sscoid  35877  bj-pwvrelb  36864  bj-elsnb  37027  bj-ideqb  37125  bj-opelidb1ALT  37132  bj-elid5  37135  eldiophb  42713  eldioph3b  42721  eldioph4b  42767  bropabg  43285  brfvrcld2  43654