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 573	. 2 ⊢ ((𝜓 → (𝜒 ↔ 𝜃)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))
3	1, 2	sylib 218	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:  pm5.32rd  578  pm5.32da  579  anbi2d  631  raltpd  4740  opeqsng  5459  dfres3  5951  cores  6215  isoini  7294  eqfunresadj  7316  mpoeq123  7440  ordpwsuc  7767  xpord3pred  8104  rdglim2  8373  fzind  12602  btwnz  12607  elfzm11  13523  isprm2  16621  isprm3  16622  modprminv  16739  modprminveq  16740  isrngim2  20401  elimifd  32629  indpi1  32951  xrecex  33011  ordtconnlem1  34101  dfrdg4  36164  ee7.2aOLD  36674  expdioph  43374  cantnf2  43676  pm14.122b  44773  rexbidar  44795