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  7355  m1p1sr  7709  m1m1sr  7710  0lt1sr  7714  axi2m1  7824  mul4i  8054  add4i  8071  addsub4i  8202  muladdi  8315  lt2addi  8416  le2addi  8417  mulap0i  8561  divap0i  8664  divmuldivapi  8676  divmul13api  8677  divadddivapi  8678  divdivdivapi  8679  subrecapi  8744  8th4div3  9084  iap0  9088  fldiv4p1lem1div2  10248  sqrt2gt1lt2  11000  abs3lemi  11108  3dvds2dec  11812  flodddiv4  11880  nprmi  12065  sinhalfpilem  13465  cos0pilt1  13526  lgsdir2lem1  13682  lgsdir2lem5  13686
  Copyright terms: Public domain W3C validator