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

Theorem pm5.21nd 802
Description: Eliminate an antecedent implied by each side of a biconditional. Variant of pm5.21ndd 379. (Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen, 4-Nov-2013.)
Hypotheses
Ref Expression
pm5.21nd.1 ((𝜑𝜓) → 𝜃)
pm5.21nd.2 ((𝜑𝜒) → 𝜃)
pm5.21nd.3 (𝜃 → (𝜓𝜒))
Assertion
Ref Expression
pm5.21nd (𝜑 → (𝜓𝜒))

Proof of Theorem pm5.21nd
StepHypRef Expression
1 pm5.21nd.1 . . 3 ((𝜑𝜓) → 𝜃)
21ex 412 . 2 (𝜑 → (𝜓𝜃))
3 pm5.21nd.2 . . 3 ((𝜑𝜒) → 𝜃)
43ex 412 . 2 (𝜑 → (𝜒𝜃))
5 pm5.21nd.3 . . 3 (𝜃 → (𝜓𝜒))
65a1i 11 . 2 (𝜑 → (𝜃 → (𝜓𝜒)))
72, 4, 6pm5.21ndd 379 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395
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 207  df-an 396
This theorem is referenced by:  ideqg  5862  fvelimab  6981  brrpssg  7745  ordsucelsuc  7842  releldm2  8068  relbrtpos  8262  relelec  8792  elfiun  9470  fpwwe2lem2  10672  fpwwelem  10685  fzrev3  13630  elfzp12  13643  eqgval  19195  ismhp  22144  eltg  22964  eltg2  22965  cncnp2  23289  isref  23517  islocfin  23525  opeldifid  32612  isfne  36340  copsex2b  37141  bj-ideqgALT  37159  bj-idreseq  37163  bj-ideqg1ALT  37166  opelopab3  37725  isdivrngo  37957  brssr  38502  islshpkrN  39121  dihatexv2  41341
  Copyright terms: Public domain W3C validator