NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  mpan9 GIF version

Theorem mpan9 455
Description: Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypotheses
Ref Expression
mpan9.1 (φψ)
mpan9.2 (χ → (ψθ))
Assertion
Ref Expression
mpan9 ((φ χ) → θ)

Proof of Theorem mpan9
StepHypRef Expression
1 mpan9.1 . . 3 (φψ)
2 mpan9.2 . . 3 (χ → (ψθ))
31, 2syl5 28 . 2 (χ → (φθ))
43impcom 419 1 ((φ χ) → θ)
Colors of variables: wff setvar class
Syntax hints:  wi 4   wa 358
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 177  df-an 360
This theorem is referenced by:  sylan  457  vtocl2gf  2916  vtocl3gf  2917  vtoclegft  2926  sbcthdv  3061  nnsucelr  4428  nnadjoin  4520  sfintfin  4532  funiunfv  5467  isorel  5489  caovcld  5622  caovcomg  5624  caovassg  5626  caovdig  5632  caovdirg  5633
  Copyright terms: Public domain W3C validator