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  5864  fvelimab  6980  brrpssg  7743  ordsucelsuc  7841  releldm2  8066  relbrtpos  8260  relelec  8790  elfiun  9467  fpwwe2lem2  10669  fpwwelem  10682  fzrev3  13626  elfzp12  13639  eqgval  19207  ismhp  22161  eltg  22979  eltg2  22980  cncnp2  23304  isref  23532  islocfin  23540  opeldifid  32618  isfne  36321  copsex2b  37122  bj-ideqgALT  37140  bj-idreseq  37144  bj-ideqg1ALT  37147  opelopab3  37704  isdivrngo  37936  brssr  38482  islshpkrN  39101  dihatexv2  41321
  Copyright terms: Public domain W3C validator