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

Theorem mp4an 424
 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 270 . 2 (𝜑𝜓)
4 mp4an.3 . . 3 𝜒
5 mp4an.4 . . 3 𝜃
64, 5pm3.2i 270 . 2 (𝜒𝜃)
7 mp4an.5 . 2 (((𝜑𝜓) ∧ (𝜒𝜃)) → 𝜏)
83, 6, 7mp2an 423 1 𝜏
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107 This theorem is referenced by:  1lt2nq  7237  m1p1sr  7591  m1m1sr  7592  0lt1sr  7596  axi2m1  7706  mul4i  7933  add4i  7950  addsub4i  8081  muladdi  8194  lt2addi  8295  le2addi  8296  mulap0i  8440  divap0i  8543  divmuldivapi  8555  divmul13api  8556  divadddivapi  8557  divdivdivapi  8558  subrecapi  8622  8th4div3  8962  iap0  8966  fldiv4p1lem1div2  10108  sqrt2gt1lt2  10852  abs3lemi  10960  3dvds2dec  11597  flodddiv4  11665  nprmi  11839  sinhalfpilem  12918  cos0pilt1  12979
 Copyright terms: Public domain W3C validator