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

Theorem mp4an 403
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 257 . 2 (𝜑𝜓)
4 mp4an.3 . . 3 𝜒
5 mp4an.4 . . 3 𝜃
64, 5pm3.2i 257 . 2 (𝜒𝜃)
7 mp4an.5 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
83, 6, 7mp2an 402 1 𝜏
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  1lt2nq  6502  m1p1sr  6843  m1m1sr  6844  0lt1sr  6848  axi2m1  6947  mul4i  7159  add4i  7174  addsub4i  7305  muladdi  7404  lt2addi  7500  le2addi  7501  mulap0i  7635  divap0i  7734  divmuldivapi  7746  divmul13api  7747  divadddivapi  7748  divdivdivapi  7749  8th4div3  8142  iap0  8146  fldiv4p1lem1div2  9145  sqrt2gt1lt2  9645  abs3lemi  9751
  Copyright terms: Public domain W3C validator