Theorem pm5.32d 577

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 29-Oct-1996.)

Hypothesis

Ref	Expression
pm5.32d.1	⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))

Assertion

Ref	Expression
pm5.32d	⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Proof of Theorem pm5.32d

Step	Hyp	Ref	Expression
1		pm5.32d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
2		pm5.32 574	. 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
3	1, 2	sylib 217	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  pm5.32rd  578  pm5.32da  579  anbi2d  629  ralrexbidOLD  3107  raltpd  4785  opeqsng  5503  dfres3  5986  cores  6248  isoini  7337  eqfunresadj  7359  mpoeq123  7483  ordpwsuc  7805  xpord3pred  8140  rdglim2  8434  fzind  12664  btwnz  12669  elfzm11  13576  isprm2  16623  isprm3  16624  modprminv  16736  modprminveq  16737  isrngim2  20344  isrimOLD  20384  elimifd  32030  xrecex  32341  ordtconnlem1  33190  indpi1  33304  dfrdg4  35215  ee7.2aOLD  35649  wl-ax11-lem8  36757  expdioph  42064  cantnf2  42377  pm14.122b  43484  rexbidar  43507