ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2falsed GIF version

Theorem 2falsed 702
Description: Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013.)
Hypotheses
Ref Expression
2falsed.1 (𝜑 → ¬ 𝜓)
2falsed.2 (𝜑 → ¬ 𝜒)
Assertion
Ref Expression
2falsed (𝜑 → (𝜓𝜒))

Proof of Theorem 2falsed
StepHypRef Expression
1 2falsed.1 . . 3 (𝜑 → ¬ 𝜓)
21pm2.21d 619 . 2 (𝜑 → (𝜓𝜒))
3 2falsed.2 . . 3 (𝜑 → ¬ 𝜒)
43pm2.21d 619 . 2 (𝜑 → (𝜒𝜓))
52, 4impbid 129 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108  ax-in2 615
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  pm5.21ni  703  bianfd  948  abvor0dc  3446  nn0eln0  4619  nntri3  6497  fin0  6884  omp1eomlem  7092  ctssdccl  7109  ismkvnex  7152  xrlttri3  9796  nltpnft  9813  ngtmnft  9816  xrrebnd  9818  xltadd1  9875  xposdif  9881  xleaddadd  9886  hashnncl  10774  zfz1isolemiso  10818  mod2eq1n2dvds  11883  m1exp1  11905  pceq0  12320
  Copyright terms: Public domain W3C validator