Theorem mp4an 427

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

Step	Hyp	Ref	Expression
1		mp4an.1	. . 3 ⊢ 𝜑
2		mp4an.2	. . 3 ⊢ 𝜓
3	1, 2	pm3.2i 272	. 2 ⊢ (𝜑 ∧ 𝜓)
4		mp4an.3	. . 3 ⊢ 𝜒
5		mp4an.4	. . 3 ⊢ 𝜃
6	4, 5	pm3.2i 272	. 2 ⊢ (𝜒 ∧ 𝜃)
7		mp4an.5	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
8	3, 6, 7	mp2an 426	1 ⊢ 𝜏

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  1lt2nq  7539  m1p1sr  7893  m1m1sr  7894  0lt1sr  7898  axi2m1  8008  mul4i  8240  add4i  8257  addsub4i  8388  muladdi  8501  lt2addi  8603  le2addi  8604  mulap0i  8749  divap0i  8853  divmuldivapi  8865  divmul13api  8866  divadddivapi  8867  divdivdivapi  8868  subrecapi  8933  8th4div3  9276  iap0  9280  fldiv4p1lem1div2  10470  sqrt2gt1lt2  11435  abs3lemi  11543  3dvds2dec  12252  flodddiv4  12322  nprmi  12521  modxai  12814  sinhalfpilem  15338  cos0pilt1  15399  lgsdir2lem1  15580  lgsdir2lem5  15584  m1lgs  15637  2lgslem4  15655