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 797
Description: Eliminate an antecedent implied by each side of a biconditional. Variant of pm5.21ndd 368. (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 397 . 2 (𝜑 → (𝜓𝜃))
3 pm5.21nd.2 . . 3 ((𝜑𝜒) → 𝜃)
43ex 397 . 2 (𝜑 → (𝜒𝜃))
5 pm5.21nd.3 . . 3 (𝜃 → (𝜓𝜒))
65a1i 11 . 2 (𝜑 → (𝜃 → (𝜓𝜒)))
72, 4, 6pm5.21ndd 368 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382
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  df-an 383
This theorem is referenced by:  ideqg  5413  fvelimab  6396  brrpssg  7087  ordsucelsuc  7170  releldm2  7368  relbrtpos  7516  relelec  7940  elfiun  8493  fpwwe2lem2  9657  fpwwelem  9670  fzrev3  12614  elfzp12  12627  eqgval  17852  eltg  20983  eltg2  20984  cncnp2  21307  isref  21534  islocfin  21542  opeldifid  29751  isfne  32672  opelopab3  33844  isdivrngo  34082  brssr  34594  islshpkrN  34930  dihatexv2  37150
  Copyright terms: Public domain W3C validator