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

Theorem mp4an 411
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 261 . 2  |-  ( ph  /\ 
ps )
4 mp4an.3 . . 3  |-  ch
5 mp4an.4 . . 3  |-  th
64, 5pm3.2i 261 . 2  |-  ( ch 
/\  th )
7 mp4an.5 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
83, 6, 7mp2an 410 1  |-  ta
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  1lt2nq  6561  m1p1sr  6902  m1m1sr  6903  0lt1sr  6907  axi2m1  7006  mul4i  7221  add4i  7238  addsub4i  7369  muladdi  7477  lt2addi  7575  le2addi  7576  mulap0i  7710  divap0i  7810  divmuldivapi  7822  divmul13api  7823  divadddivapi  7824  divdivdivapi  7825  8th4div3  8200  iap0  8204  fldiv4p1lem1div2  9249  sqrt2gt1lt2  9868  abs3lemi  9976  3dvds2dec  10169
  Copyright terms: Public domain W3C validator