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  7468  m1p1sr  7822  m1m1sr  7823  0lt1sr  7827  axi2m1  7937  mul4i  8169  add4i  8186  addsub4i  8317  muladdi  8430  lt2addi  8531  le2addi  8532  mulap0i  8677  divap0i  8781  divmuldivapi  8793  divmul13api  8794  divadddivapi  8795  divdivdivapi  8796  subrecapi  8861  8th4div3  9204  iap0  9208  fldiv4p1lem1div2  10377  sqrt2gt1lt2  11196  abs3lemi  11304  3dvds2dec  12010  flodddiv4  12078  nprmi  12265  sinhalfpilem  14958  cos0pilt1  15019  lgsdir2lem1  15176  lgsdir2lem5  15180  m1lgs  15233  2lgslem4  15251