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  7404  m1p1sr  7758  m1m1sr  7759  0lt1sr  7763  axi2m1  7873  mul4i  8104  add4i  8121  addsub4i  8252  muladdi  8365  lt2addi  8466  le2addi  8467  mulap0i  8612  divap0i  8716  divmuldivapi  8728  divmul13api  8729  divadddivapi  8730  divdivdivapi  8731  subrecapi  8796  8th4div3  9137  iap0  9141  fldiv4p1lem1div2  10304  sqrt2gt1lt2  11057  abs3lemi  11165  3dvds2dec  11870  flodddiv4  11938  nprmi  12123  sinhalfpilem  14182  cos0pilt1  14243  lgsdir2lem1  14399  lgsdir2lem5  14403  m1lgs  14422
  Copyright terms: Public domain W3C validator