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

Theorem mp4an 427
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 272 . 2 (𝜑𝜓)
4 mp4an.3 . . 3 𝜒
5 mp4an.4 . . 3 𝜃
64, 5pm3.2i 272 . 2 (𝜒𝜃)
7 mp4an.5 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
83, 6, 7mp2an 426 1 𝜏
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  7383  m1p1sr  7737  m1m1sr  7738  0lt1sr  7742  axi2m1  7852  mul4i  8082  add4i  8099  addsub4i  8230  muladdi  8343  lt2addi  8444  le2addi  8445  mulap0i  8589  divap0i  8693  divmuldivapi  8705  divmul13api  8706  divadddivapi  8707  divdivdivapi  8708  subrecapi  8773  8th4div3  9114  iap0  9118  fldiv4p1lem1div2  10278  sqrt2gt1lt2  11029  abs3lemi  11137  3dvds2dec  11841  flodddiv4  11909  nprmi  12094  sinhalfpilem  13845  cos0pilt1  13906  lgsdir2lem1  14062  lgsdir2lem5  14066
  Copyright terms: Public domain W3C validator