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  6504  m1p1sr  6845  m1m1sr  6846  0lt1sr  6850  axi2m1  6949  mul4i  7161  add4i  7176  addsub4i  7307  muladdi  7406  lt2addi  7502  le2addi  7503  mulap0i  7637  divap0i  7736  divmuldivapi  7748  divmul13api  7749  divadddivapi  7750  divdivdivapi  7751  8th4div3  8144  iap0  8148  fldiv4p1lem1div2  9147  sqrt2gt1lt2  9647  abs3lemi  9753
 Copyright terms: Public domain W3C validator