Theorem pm5.32da 456

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 454	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  rexbida  2545  reubida  2734  rmobida  2740  mpteq12f  4211  reuhypd  4617  funbrfv2b  5747  dffn5im  5748  eqfnfv2  5807  fndmin  5816  fniniseg  5829  fmptco  5874  dff13  5974  riotabidva  6056  mpoeq123dva  6149  mpoeq3dva  6152  suppssrst  6501  suppssrgst  6502  mpoxopovel  6512  qliftfun  6891  erovlem  6901  mapsnend  7099  xpcomco  7124  pw2f1odclem  7134  elfi2  7306  ctssdccl  7451  ltexpi  7704  dfplpq2  7721  axprecex  8247  zrevaddcl  9697  qrevaddcl  10046  icoshft  10394  fznn  10498  sseqn  11281  pfxeq  11470  pfxsuffeqwrdeq  11472  pfxsuff1eqwrdeq  11473  shftdm  11589  2shfti  11598  sumeq2  12127  fsum3  12156  fsum2dlemstep  12203  prodeq2  12326  fprodseq  12352  bitsmod  12725  bitscmp  12727  gcdaddm  12763  grpidpropdg  13696  ismgmid  13699  mhmpropd  13775  issubm2  13782  eqgid  14031  eqgabl  14136  rngpropd  14256  iscrng2  14321  ringpropd  14345  crngpropd  14346  crngunit  14420  dvdsrpropdg  14456  issubrg3  14557  lsslss  14720  lsspropdg  14770  znleval  14990  bastop2  15187  restopn2  15286  iscnp3  15306  lmbr2  15317  txlm  15382  ismet2  15457  xblpnfps  15501  xblpnf  15502  blininf  15527  blres  15537  elmopn2  15552  neibl  15594  metrest  15609  metcnp3  15614  metcnp  15615  metcnp2  15616  metcn  15617  txmetcn  15622  cnbl0  15637  cnblcld  15638  bl2ioo  15653  elcncf2  15677  cncfmet  15695  cnlimc  15775  lgsquadlem1  16208  lgsquadlem2  16209  2lgslem1a  16219  upgriswlkdc  16613  isclwwlknx  16669  clwwlkn1  16671  clwwlkn2  16674  eupth2lemsfi  16731