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

Theorem mp4an 421
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 268 . 2  |-  ( ph  /\ 
ps )
4 mp4an.3 . . 3  |-  ch
5 mp4an.4 . . 3  |-  th
64, 5pm3.2i 268 . 2  |-  ( ch 
/\  th )
7 mp4an.5 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
83, 6, 7mp2an 420 1  |-  ta
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-ia3 107
This theorem is referenced by:  1lt2nq  7178  m1p1sr  7532  m1m1sr  7533  0lt1sr  7537  axi2m1  7647  mul4i  7874  add4i  7891  addsub4i  8022  muladdi  8135  lt2addi  8236  le2addi  8237  mulap0i  8377  divap0i  8480  divmuldivapi  8492  divmul13api  8493  divadddivapi  8494  divdivdivapi  8495  8th4div3  8890  iap0  8894  fldiv4p1lem1div2  10018  sqrt2gt1lt2  10761  abs3lemi  10869  3dvds2dec  11459  flodddiv4  11527  nprmi  11701
  Copyright terms: Public domain W3C validator