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

Theorem mpan9 279
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 124 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem is referenced by:  sylan  281  vtocl2gf  2748  vtocl3gf  2749  vtoclegft  2758  sbcthdv  2923  disji2  3922  swopolem  4227  funssres  5165  fvmptssdm  5505  fmptcof  5587  fliftfuns  5699  isorel  5709  caovclg  5923  caovcomg  5926  caovassg  5929  caovcang  5932  caovordig  5936  caovordg  5938  caovdig  5945  caovdirg  5948  qliftfuns  6513  nneneq  6751  supmoti  6880  exmidonfinlem  7054  recexprlemopl  7445  recexprlemopu  7447  cauappcvgprlemladdrl  7477  caucvgsrlemcl  7609  caucvgsrlemfv  7611  caucvgsr  7622  suplocsrlempr  7627  ltordlem  8256  lble  8717  uz11  9360  seq3caopr3  10266  climcaucn  11132  sumdc  11139  fsum3  11168  fsumf1o  11171  fsum3cvg2  11175  isummulc2  11207  fsum2dlemstep  11215  fisumcom2  11219  fsumshftm  11226  fisum0diag2  11228  fsum00  11243  isumshft  11271  clim2prod  11320  prodmodclem2  11358  dvdsprm  11828  ssnei2  12340  psmet0  12510  psmettri2  12511  cncfi  12748  dvcn  12847  exmid1stab  13254  nninfsellemdc  13267
  Copyright terms: Public domain W3C validator