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  7609  m1p1sr  7963  m1m1sr  7964  0lt1sr  7968  axi2m1  8078  mul4i  8310  add4i  8327  addsub4i  8458  muladdi  8571  lt2addi  8673  le2addi  8674  mulap0i  8819  divap0i  8923  divmuldivapi  8935  divmul13api  8936  divadddivapi  8937  divdivdivapi  8938  subrecapi  9003  8th4div3  9346  iap0  9350  fldiv4p1lem1div2  10542  sqrt2gt1lt2  11581  abs3lemi  11689  3dvds2dec  12398  flodddiv4  12468  nprmi  12667  modxai  12960  sinhalfpilem  15486  cos0pilt1  15547  lgsdir2lem1  15728  lgsdir2lem5  15732  m1lgs  15785  2lgslem4  15803