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  2539  reubida  2728  rmobida  2734  mpteq12f  4195  reuhypd  4597  funbrfv2b  5726  dffn5im  5727  eqfnfv2  5781  fndmin  5790  fniniseg  5803  fmptco  5848  dff13  5947  riotabidva  6029  mpoeq123dva  6122  mpoeq3dva  6125  suppssrst  6474  suppssrgst  6475  mpoxopovel  6485  qliftfun  6864  erovlem  6874  mapsnend  7065  xpcomco  7090  pw2f1odclem  7100  elfi2  7272  ctssdccl  7415  ltexpi  7668  dfplpq2  7685  axprecex  8211  zrevaddcl  9645  qrevaddcl  9994  icoshft  10342  fznn  10445  sseqn  11228  pfxeq  11413  pfxsuffeqwrdeq  11415  pfxsuff1eqwrdeq  11416  shftdm  11532  2shfti  11541  sumeq2  12069  fsum3  12098  fsum2dlemstep  12145  prodeq2  12268  fprodseq  12294  bitsmod  12667  bitscmp  12669  gcdaddm  12705  grpidpropdg  13671  ismgmid  13674  gsumpropd2  13690  mhmpropd  13763  issubm2  13770  eqgid  14027  eqgabl  14131  rngpropd  14183  iscrng2  14243  ringpropd  14266  crngpropd  14267  crngunit  14341  dvdsrpropdg  14377  issubrg3  14478  lsslss  14641  lsspropdg  14691  znleval  14913  bastop2  15061  restopn2  15160  iscnp3  15180  lmbr2  15191  txlm  15256  ismet2  15331  xblpnfps  15375  xblpnf  15376  blininf  15401  blres  15411  elmopn2  15426  neibl  15468  metrest  15483  metcnp3  15488  metcnp  15489  metcnp2  15490  metcn  15491  txmetcn  15496  cnbl0  15511  cnblcld  15512  bl2ioo  15527  elcncf2  15551  cncfmet  15569  cnlimc  15649  lgsquadlem1  16062  lgsquadlem2  16063  2lgslem1a  16073  upgriswlkdc  16467  isclwwlknx  16523  clwwlkn1  16525  clwwlkn2  16528  eupth2lemsfi  16585