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  7669  m1p1sr  8023  m1m1sr  8024  0lt1sr  8028  axi2m1  8138  mul4i  8369  add4i  8386  addsub4i  8517  muladdi  8630  lt2addi  8732  le2addi  8733  mulap0i  8878  divap0i  8982  divmuldivapi  8994  divmul13api  8995  divadddivapi  8996  divdivdivapi  8997  subrecapi  9062  8th4div3  9405  iap0  9409  fldiv4p1lem1div2  10611  sqrt2gt1lt2  11672  abs3lemi  11780  3dvds2dec  12490  flodddiv4  12560  nprmi  12759  modxai  13052  sinhalfpilem  15585  cos0pilt1  15646  lgsdir2lem1  15830  lgsdir2lem5  15834  m1lgs  15887  2lgslem4  15905