ILE Home 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  6912  m1p1sr  7253  m1m1sr  7254  0lt1sr  7258  axi2m1  7357  mul4i  7577  add4i  7594  addsub4i  7725  muladdi  7834  lt2addi  7932  le2addi  7933  mulap0i  8067  divap0i  8169  divmuldivapi  8181  divmul13api  8182  divadddivapi  8183  divdivdivapi  8184  8th4div3  8571  iap0  8575  fldiv4p1lem1div2  9643  sqrt2gt1lt2  10381  abs3lemi  10489  3dvds2dec  10772  flodddiv4  10840  nprmi  11012
  Copyright terms: Public domain W3C validator