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

Theorem mp4an 425
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 270 . 2  |-  ( ph  /\ 
ps )
4 mp4an.3 . . 3  |-  ch
5 mp4an.4 . . 3  |-  th
64, 5pm3.2i 270 . 2  |-  ( ch 
/\  th )
7 mp4an.5 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
83, 6, 7mp2an 424 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  7368  m1p1sr  7722  m1m1sr  7723  0lt1sr  7727  axi2m1  7837  mul4i  8067  add4i  8084  addsub4i  8215  muladdi  8328  lt2addi  8429  le2addi  8430  mulap0i  8574  divap0i  8677  divmuldivapi  8689  divmul13api  8690  divadddivapi  8691  divdivdivapi  8692  subrecapi  8757  8th4div3  9097  iap0  9101  fldiv4p1lem1div2  10261  sqrt2gt1lt2  11013  abs3lemi  11121  3dvds2dec  11825  flodddiv4  11893  nprmi  12078  sinhalfpilem  13506  cos0pilt1  13567  lgsdir2lem1  13723  lgsdir2lem5  13727
  Copyright terms: Public domain W3C validator