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  7400  m1p1sr  7754  m1m1sr  7755  0lt1sr  7759  axi2m1  7869  mul4i  8099  add4i  8116  addsub4i  8247  muladdi  8360  lt2addi  8461  le2addi  8462  mulap0i  8607  divap0i  8711  divmuldivapi  8723  divmul13api  8724  divadddivapi  8725  divdivdivapi  8726  subrecapi  8791  8th4div3  9132  iap0  9136  fldiv4p1lem1div2  10298  sqrt2gt1lt2  11049  abs3lemi  11157  3dvds2dec  11861  flodddiv4  11929  nprmi  12114  sinhalfpilem  13994  cos0pilt1  14055  lgsdir2lem1  14211  lgsdir2lem5  14215