ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpan9 GIF 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 (𝜑𝜓)
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 123 1 ((𝜑𝜒) → 𝜃)
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  2674  vtocl3gf  2675  vtoclegft  2684  sbcthdv  2843  swopolem  4106  funssres  5021  fvmptssdm  5350  fmptcof  5428  fliftfuns  5538  isorel  5548  caovclg  5754  caovcomg  5757  caovassg  5760  caovcang  5763  caovordig  5767  caovordg  5769  caovdig  5776  caovdirg  5779  qliftfuns  6328  nneneq  6525  supmoti  6632  recexprlemopl  7128  recexprlemopu  7130  cauappcvgprlemladdrl  7160  caucvgsrlemcl  7278  caucvgsrlemfv  7280  caucvgsr  7291  lble  8343  uz11  8973  iseqfeq  9806  iseqcaopr3  9815  climcaucn  10632  sumdc  10639  fisum  10667  fsumf1o  10670  fisumcvg2  10674  dvdsprm  11000  nninfsellemdc  11347
  Copyright terms: Public domain W3C validator