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

Theorem mp4an 418
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 266 . 2  |-  ( ph  /\ 
ps )
4 mp4an.3 . . 3  |-  ch
5 mp4an.4 . . 3  |-  th
64, 5pm3.2i 266 . 2  |-  ( ch 
/\  th )
7 mp4an.5 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
83, 6, 7mp2an 417 1  |-  ta
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  1lt2nq  6963  m1p1sr  7304  m1m1sr  7305  0lt1sr  7309  axi2m1  7408  mul4i  7628  add4i  7645  addsub4i  7776  muladdi  7885  lt2addi  7986  le2addi  7987  mulap0i  8123  divap0i  8225  divmuldivapi  8237  divmul13api  8238  divadddivapi  8239  divdivdivapi  8240  8th4div3  8633  iap0  8637  fldiv4p1lem1div2  9708  sqrt2gt1lt2  10478  abs3lemi  10586  3dvds2dec  11140  flodddiv4  11208  nprmi  11380
  Copyright terms: Public domain W3C validator