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

Theorem pm5.21nd 801
 Description: Eliminate an antecedent implied by each side of a biconditional. Variant of pm5.21ndd 384. (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 416 . 2 (𝜑 → (𝜓𝜃))
3 pm5.21nd.2 . . 3 ((𝜑𝜒) → 𝜃)
43ex 416 . 2 (𝜑 → (𝜒𝜃))
5 pm5.21nd.3 . . 3 (𝜃 → (𝜓𝜒))
65a1i 11 . 2 (𝜑 → (𝜃 → (𝜓𝜒)))
72, 4, 6pm5.21ndd 384 1 (𝜑 → (𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  ideqg  5686  fvelimab  6712  brrpssg  7433  ordsucelsuc  7519  releldm2  7726  relbrtpos  7888  relelec  8319  elfiun  8880  fpwwe2lem2  10045  fpwwelem  10058  fzrev3  12970  elfzp12  12983  eqgval  18324  eltg  21569  eltg2  21570  cncnp2  21893  isref  22121  islocfin  22129  opeldifid  30369  isfne  33812  copsex2b  34571  bj-ideqgALT  34589  bj-idreseq  34593  bj-ideqg1ALT  34596  opelopab3  35171  isdivrngo  35404  brssr  35917  islshpkrN  36432  dihatexv2  38651
 Copyright terms: Public domain W3C validator