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

Theorem mp4an 418
 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 266 . 2 (𝜑𝜓)
4 mp4an.3 . . 3 𝜒
5 mp4an.4 . . 3 𝜃
64, 5pm3.2i 266 . 2 (𝜒𝜃)
7 mp4an.5 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
83, 6, 7mp2an 417 1 𝜏
 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  6647  m1p1sr  6988  m1m1sr  6989  0lt1sr  6993  axi2m1  7092  mul4i  7312  add4i  7329  addsub4i  7460  muladdi  7569  lt2addi  7667  le2addi  7668  mulap0i  7802  divap0i  7904  divmuldivapi  7916  divmul13api  7917  divadddivapi  7918  divdivdivapi  7919  8th4div3  8306  iap0  8310  fldiv4p1lem1div2  9376  sqrt2gt1lt2  10062  abs3lemi  10170  3dvds2dec  10399  flodddiv4  10467  nprmi  10639
 Copyright terms: Public domain W3C validator