ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpan9 GIF 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 (𝜑𝜓)
mpan9.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
mpan9 ((𝜑𝜒) → 𝜃)

Proof of Theorem mpan9
StepHypRef Expression
1 mpan9.1 . . 3 (𝜑𝜓)
2 mpan9.2 . . 3 (𝜒 → (𝜓𝜃))
31, 2syl5 32 . 2 (𝜒 → (𝜑𝜃))
43impcom 124 1 ((𝜑𝜒) → 𝜃)
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  2751  vtocl3gf  2752  vtoclegft  2761  sbcthdv  2926  disji2  3929  swopolem  4234  funssres  5172  fvmptssdm  5512  fmptcof  5594  fliftfuns  5706  isorel  5716  caovclg  5930  caovcomg  5933  caovassg  5936  caovcang  5939  caovordig  5943  caovordg  5945  caovdig  5952  caovdirg  5955  qliftfuns  6520  nneneq  6758  supmoti  6887  exmidonfinlem  7065  recexprlemopl  7456  recexprlemopu  7458  cauappcvgprlemladdrl  7488  caucvgsrlemcl  7620  caucvgsrlemfv  7622  caucvgsr  7633  suplocsrlempr  7638  ltordlem  8267  lble  8728  uz11  9371  seq3caopr3  10284  climcaucn  11151  sumdc  11158  fsum3  11187  fsumf1o  11190  fsum3cvg2  11194  isummulc2  11226  fsum2dlemstep  11234  fisumcom2  11238  fsumshftm  11245  fisum0diag2  11247  fsum00  11262  isumshft  11290  clim2prod  11339  prodmodclem2  11377  zproddc  11379  dvdsprm  11851  ssnei2  12363  psmet0  12533  psmettri2  12534  cncfi  12771  dvcn  12870  exmid1stab  13366  nninfsellemdc  13379
  Copyright terms: Public domain W3C validator