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  2525  reubida  2713  rmobida  2719  mpteq12f  4164  reuhypd  4563  funbrfv2b  5683  dffn5im  5684  eqfnfv2  5738  fndmin  5747  fniniseg  5760  rexsupp  5764  fmptco  5806  dff13  5901  riotabidva  5981  mpoeq123dva  6074  mpoeq3dva  6077  mpoxopovel  6398  qliftfun  6777  erovlem  6787  xpcomco  6998  pw2f1odclem  7008  elfi2  7155  ctssdccl  7294  ltexpi  7540  dfplpq2  7557  axprecex  8083  zrevaddcl  9513  qrevaddcl  9856  icoshft  10203  fznn  10302  pfxeq  11249  pfxsuffeqwrdeq  11251  pfxsuff1eqwrdeq  11252  shftdm  11354  2shfti  11363  sumeq2  11891  fsum3  11919  fsum2dlemstep  11966  prodeq2  12089  fprodseq  12115  bitsmod  12488  bitscmp  12490  gcdaddm  12526  grpidpropdg  13428  ismgmid  13431  gsumpropd2  13447  mhmpropd  13520  issubm2  13527  eqgid  13784  eqgabl  13888  rngpropd  13939  iscrng2  13999  ringpropd  14022  crngpropd  14023  crngunit  14096  dvdsrpropdg  14132  issubrg3  14232  lsslss  14366  lsspropdg  14416  znleval  14638  bastop2  14779  restopn2  14878  iscnp3  14898  lmbr2  14909  txlm  14974  ismet2  15049  xblpnfps  15093  xblpnf  15094  blininf  15119  blres  15129  elmopn2  15144  neibl  15186  metrest  15201  metcnp3  15206  metcnp  15207  metcnp2  15208  metcn  15209  txmetcn  15214  cnbl0  15229  cnblcld  15230  bl2ioo  15245  elcncf2  15269  cncfmet  15287  cnlimc  15367  lgsquadlem1  15777  lgsquadlem2  15778  2lgslem1a  15788  upgriswlkdc  16132  isclwwlknx  16184  clwwlkn1  16186  clwwlkn2  16189