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

Theorem 2falsed 692
 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 609 . 2 (𝜑 → (𝜓𝜒))
3 2falsed.2 . . 3 (𝜑 → ¬ 𝜒)
43pm2.21d 609 . 2 (𝜑 → (𝜒𝜓))
52, 4impbid 128 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107  ax-in2 605 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  pm5.21ni  693  bianfd  933  abvor0dc  3391  nn0eln0  4541  nntri3  6401  fin0  6787  omp1eomlem  6987  ctssdccl  7004  ismkvnex  7037  xrlttri3  9614  nltpnft  9628  ngtmnft  9631  xrrebnd  9633  xltadd1  9690  xposdif  9696  xleaddadd  9701  hashnncl  10575  zfz1isolemiso  10615  mod2eq1n2dvds  11613  m1exp1  11635
 Copyright terms: Public domain W3C validator