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  2722  vtocl3gf  2723  vtoclegft  2732  sbcthdv  2896  disji2  3892  swopolem  4197  funssres  5135  fvmptssdm  5473  fmptcof  5555  fliftfuns  5667  isorel  5677  caovclg  5891  caovcomg  5894  caovassg  5897  caovcang  5900  caovordig  5904  caovordg  5906  caovdig  5913  caovdirg  5916  qliftfuns  6481  nneneq  6719  supmoti  6848  exmidonfinlem  7017  recexprlemopl  7401  recexprlemopu  7403  cauappcvgprlemladdrl  7433  caucvgsrlemcl  7565  caucvgsrlemfv  7567  caucvgsr  7578  suplocsrlempr  7583  ltordlem  8212  lble  8673  uz11  9316  seq3caopr3  10222  climcaucn  11088  sumdc  11095  fsum3  11124  fsumf1o  11127  fsum3cvg2  11131  isummulc2  11163  fsum2dlemstep  11171  fisumcom2  11175  fsumshftm  11182  fisum0diag2  11184  fsum00  11199  isumshft  11227  dvdsprm  11744  ssnei2  12253  psmet0  12423  psmettri2  12424  cncfi  12661  dvcn  12760  exmid1stab  13122  nninfsellemdc  13133
  Copyright terms: Public domain W3C validator