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

Theorem pm5.74da 803
 Description: Distribution of implication over biconditional (deduction form). Variant of pm5.74d 276. (Contributed by NM, 4-May-2007.)
Hypothesis
Ref Expression
pm5.74da.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
pm5.74da (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))

Proof of Theorem pm5.74da
StepHypRef Expression
1 pm5.74da.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21ex 416 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32pm5.74d 276 1 (𝜑 → ((𝜓𝜒) ↔ (𝜓𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  cbvaldvaw  2045  sb4b  2491  sb4bOLD  2492  ralbidva  3164  ralbida  3197  vtocl2d  3508  vtocl2  3512  vtocl3  3514  spc3egv  3555  ralxpxfr2d  3590  elrab3t  3630  vtocl2dOLD  3879  csbie2df  4351  ordunisuc2  7543  dfom2  7566  pwfseqlem3  10075  lo1resb  14917  rlimresb  14918  o1resb  14919  fsumparts  15157  isprm3  16021  ramval  16338  islindf4  20531  cnntr  21884  fclsbas  22630  metcnp  23152  voliunlem3  24160  ellimc2  24484  limcflf  24488  mdegleb  24669  xrlimcnp  25558  dchrelbas3  25826  lmicom  26586  dmdbr5ati  30209  isarchi3  30870  islinds5  30987  cmpcref  31207  sscoid  33488  cdlemefrs29bpre0  37691  cdlemkid3N  38228  cdlemkid4  38229  hdmap1eulem  39117  hdmap1eulemOLDN  39118  jm2.25  39937  ntrneik2  40792  ntrneix2  40793  ntrneikb  40794  fourierdlem87  42832
 Copyright terms: Public domain W3C validator