ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpan9 Unicode version

Theorem mpan9 275
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  |-  ( ph  ->  ps )
mpan9.2  |-  ( ch 
->  ( ps  ->  th )
)
Assertion
Ref Expression
mpan9  |-  ( (
ph  /\  ch )  ->  th )

Proof of Theorem mpan9
StepHypRef Expression
1 mpan9.1 . . 3  |-  ( ph  ->  ps )
2 mpan9.2 . . 3  |-  ( ch 
->  ( ps  ->  th )
)
31, 2syl5 32 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43impcom 123 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem is referenced by:  sylan  277  vtocl2gf  2661  vtocl3gf  2662  vtoclegft  2671  sbcthdv  2830  swopolem  4068  funssres  4972  fvmptssdm  5287  fmptcof  5363  fliftfuns  5469  isorel  5479  caovclg  5684  caovcomg  5687  caovassg  5690  caovcang  5693  caovordig  5697  caovordg  5699  caovdig  5706  caovdirg  5709  qliftfuns  6256  nneneq  6392  supmoti  6465  recexprlemopl  6877  recexprlemopu  6879  cauappcvgprlemladdrl  6909  caucvgsrlemcl  7027  caucvgsrlemfv  7029  caucvgsr  7040  lble  8092  uz11  8722  iseqfeq  9547  iseqcaopr3  9556  climcaucn  10326  sumdc  10333  dvdsprm  10662
  Copyright terms: Public domain W3C validator