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  2681  vtocl3gf  2682  vtoclegft  2691  sbcthdv  2852  disji2  3830  swopolem  4123  funssres  5042  fvmptssdm  5371  fmptcof  5449  fliftfuns  5559  isorel  5569  caovclg  5779  caovcomg  5782  caovassg  5785  caovcang  5788  caovordig  5792  caovordg  5794  caovdig  5801  caovdirg  5804  qliftfuns  6356  nneneq  6553  supmoti  6667  recexprlemopl  7163  recexprlemopu  7165  cauappcvgprlemladdrl  7195  caucvgsrlemcl  7313  caucvgsrlemfv  7315  caucvgsr  7326  lble  8380  uz11  9010  iseqfeq  9861  iseqcaopr3  9875  climcaucn  10704  sumdc  10711  fisum  10742  fsumf1o  10746  fisumcvg2  10750  isummulc2  10783  fsum2dlemstep  10791  fisumcom2  10795  fsumshftm  10802  fisum0diag2  10804  fsum00  10819  isumshft  10846  dvdsprm  11200  nninfsellemdc  11548
  Copyright terms: Public domain W3C validator