Theorem pm5.32da 452

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 9-Dec-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem pm5.32da

Step	Hyp	Ref	Expression
1		pm5.32da.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃))
2	1	ex 115	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
3	2	pm5.32d 450	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  rexbida  2492  reubida  2679  rmobida  2684  mpteq12f  4114  reuhypd  4507  funbrfv2b  5608  dffn5im  5609  eqfnfv2  5663  fndmin  5672  fniniseg  5685  rexsupp  5689  fmptco  5731  dff13  5818  riotabidva  5897  mpoeq123dva  5987  mpoeq3dva  5990  mpoxopovel  6308  qliftfun  6685  erovlem  6695  xpcomco  6894  pw2f1odclem  6904  elfi2  7047  ctssdccl  7186  ltexpi  7423  dfplpq2  7440  axprecex  7966  zrevaddcl  9395  qrevaddcl  9737  icoshft  10084  fznn  10183  shftdm  11006  2shfti  11015  sumeq2  11543  fsum3  11571  fsum2dlemstep  11618  prodeq2  11741  fprodseq  11767  bitsmod  12140  bitscmp  12142  gcdaddm  12178  grpidpropdg  13078  ismgmid  13081  gsumpropd2  13097  mhmpropd  13170  issubm2  13177  eqgid  13434  eqgabl  13538  rngpropd  13589  iscrng2  13649  ringpropd  13672  crngpropd  13673  crngunit  13745  dvdsrpropdg  13781  issubrg3  13881  lsslss  14015  lsspropdg  14065  znleval  14287  bastop2  14428  restopn2  14527  iscnp3  14547  lmbr2  14558  txlm  14623  ismet2  14698  xblpnfps  14742  xblpnf  14743  blininf  14768  blres  14778  elmopn2  14793  neibl  14835  metrest  14850  metcnp3  14855  metcnp  14856  metcnp2  14857  metcn  14858  txmetcn  14863  cnbl0  14878  cnblcld  14879  bl2ioo  14894  elcncf2  14918  cncfmet  14936  cnlimc  15016  lgsquadlem1  15426  lgsquadlem2  15427  2lgslem1a  15437