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

Theorem mp4an 424
 Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2011.)
Hypotheses
Ref Expression
mp4an.1
mp4an.2
mp4an.3
mp4an.4
mp4an.5
Assertion
Ref Expression
mp4an

Proof of Theorem mp4an
StepHypRef Expression
1 mp4an.1 . . 3
2 mp4an.2 . . 3
31, 2pm3.2i 270 . 2
4 mp4an.3 . . 3
5 mp4an.4 . . 3
64, 5pm3.2i 270 . 2
7 mp4an.5 . 2
83, 6, 7mp2an 423 1
 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  7258  m1p1sr  7612  m1m1sr  7613  0lt1sr  7617  axi2m1  7727  mul4i  7954  add4i  7971  addsub4i  8102  muladdi  8215  lt2addi  8316  le2addi  8317  mulap0i  8461  divap0i  8564  divmuldivapi  8576  divmul13api  8577  divadddivapi  8578  divdivdivapi  8579  subrecapi  8643  8th4div3  8983  iap0  8987  fldiv4p1lem1div2  10129  sqrt2gt1lt2  10873  abs3lemi  10981  3dvds2dec  11619  flodddiv4  11687  nprmi  11861  sinhalfpilem  12940  cos0pilt1  13001
 Copyright terms: Public domain W3C validator