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  2527  reubida  2715  rmobida  2721  mpteq12f  4169  reuhypd  4568  funbrfv2b  5690  dffn5im  5691  eqfnfv2  5745  fndmin  5754  fniniseg  5767  rexsupp  5771  fmptco  5813  dff13  5909  riotabidva  5989  mpoeq123dva  6082  mpoeq3dva  6085  mpoxopovel  6407  qliftfun  6786  erovlem  6796  xpcomco  7010  pw2f1odclem  7020  elfi2  7171  ctssdccl  7310  ltexpi  7557  dfplpq2  7574  axprecex  8100  zrevaddcl  9530  qrevaddcl  9878  icoshft  10225  fznn  10324  pfxeq  11278  pfxsuffeqwrdeq  11280  pfxsuff1eqwrdeq  11281  shftdm  11384  2shfti  11393  sumeq2  11921  fsum3  11950  fsum2dlemstep  11997  prodeq2  12120  fprodseq  12146  bitsmod  12519  bitscmp  12521  gcdaddm  12557  grpidpropdg  13459  ismgmid  13462  gsumpropd2  13478  mhmpropd  13551  issubm2  13558  eqgid  13815  eqgabl  13919  rngpropd  13971  iscrng2  14031  ringpropd  14054  crngpropd  14055  crngunit  14128  dvdsrpropdg  14164  issubrg3  14264  lsslss  14398  lsspropdg  14448  znleval  14670  bastop2  14811  restopn2  14910  iscnp3  14930  lmbr2  14941  txlm  15006  ismet2  15081  xblpnfps  15125  xblpnf  15126  blininf  15151  blres  15161  elmopn2  15176  neibl  15218  metrest  15233  metcnp3  15238  metcnp  15239  metcnp2  15240  metcn  15241  txmetcn  15246  cnbl0  15261  cnblcld  15262  bl2ioo  15277  elcncf2  15301  cncfmet  15319  cnlimc  15399  lgsquadlem1  15809  lgsquadlem2  15810  2lgslem1a  15820  upgriswlkdc  16214  isclwwlknx  16270  clwwlkn1  16272  clwwlkn2  16275  eupth2lemsfi  16332