MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm5.74d Structured version   Visualization version   GIF version

Theorem pm5.74d 262
Description: Distribution of implication over biconditional (deduction rule). (Contributed by NM, 21-Mar-1996.)
Hypothesis
Ref Expression
pm5.74d.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
pm5.74d (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))

Proof of Theorem pm5.74d
StepHypRef Expression
1 pm5.74d.1 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
2 pm5.74 259 . 2 ((𝜓 → (𝜒𝜃)) ↔ ((𝜓𝜒) ↔ (𝜓𝜃)))
31, 2sylib 208 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  imbi2d  330  imim21b  382  pm5.74da  722  cbval2  2277  cbvaldva  2279  dvelimdf  2333  sbied  2407  dfiin2g  4544  oneqmini  5764  tfindsg  7045  findsg  7078  brecop  7825  dom2lem  7980  indpi  9714  nn0ind-raph  11462  cncls2  21058  ismbl2  23276  voliunlem3  23301  mdbr2  29125  dmdbr2  29132  mdsl2i  29151  mdsl2bi  29152  sgn3da  30577  bj-cbval2v  32712  wl-dral1d  33289  wl-equsald  33296  cvlsupr3  34450  cdleme32fva  35544  cdlemk33N  36016  cdlemk34  36017  ralbidar  38469  tfis2d  42192
  Copyright terms: Public domain W3C validator