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

Theorem mp4an 427
Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2011.)
Hypotheses
Ref Expression
mp4an.1  |-  ph
mp4an.2  |-  ps
mp4an.3  |-  ch
mp4an.4  |-  th
mp4an.5  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
Assertion
Ref Expression
mp4an  |-  ta

Proof of Theorem mp4an
StepHypRef Expression
1 mp4an.1 . . 3  |-  ph
2 mp4an.2 . . 3  |-  ps
31, 2pm3.2i 272 . 2  |-  ( ph  /\ 
ps )
4 mp4an.3 . . 3  |-  ch
5 mp4an.4 . . 3  |-  th
64, 5pm3.2i 272 . 2  |-  ( ch 
/\  th )
7 mp4an.5 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
83, 6, 7mp2an 426 1  |-  ta
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108
This theorem is referenced by:  1lt2nq  7435  m1p1sr  7789  m1m1sr  7790  0lt1sr  7794  axi2m1  7904  mul4i  8135  add4i  8152  addsub4i  8283  muladdi  8396  lt2addi  8497  le2addi  8498  mulap0i  8643  divap0i  8747  divmuldivapi  8759  divmul13api  8760  divadddivapi  8761  divdivdivapi  8762  subrecapi  8827  8th4div3  9168  iap0  9172  fldiv4p1lem1div2  10336  sqrt2gt1lt2  11090  abs3lemi  11198  3dvds2dec  11903  flodddiv4  11971  nprmi  12156  sinhalfpilem  14669  cos0pilt1  14730  lgsdir2lem1  14887  lgsdir2lem5  14891  m1lgs  14910
  Copyright terms: Public domain W3C validator