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  7405  m1p1sr  7759  m1m1sr  7760  0lt1sr  7764  axi2m1  7874  mul4i  8105  add4i  8122  addsub4i  8253  muladdi  8366  lt2addi  8467  le2addi  8468  mulap0i  8613  divap0i  8717  divmuldivapi  8729  divmul13api  8730  divadddivapi  8731  divdivdivapi  8732  subrecapi  8797  8th4div3  9138  iap0  9142  fldiv4p1lem1div2  10305  sqrt2gt1lt2  11058  abs3lemi  11166  3dvds2dec  11871  flodddiv4  11939  nprmi  12124  sinhalfpilem  14215  cos0pilt1  14276  lgsdir2lem1  14432  lgsdir2lem5  14436  m1lgs  14455
  Copyright terms: Public domain W3C validator