Theorem mp4an 423

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 270	. 2 ⊢ (𝜑 ∧ 𝜓)
4		mp4an.3	. . 3 ⊢ 𝜒
5		mp4an.4	. . 3 ⊢ 𝜃
6	4, 5	pm3.2i 270	. 2 ⊢ (𝜒 ∧ 𝜃)
7		mp4an.5	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
8	3, 6, 7	mp2an 422	1 ⊢ 𝜏

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  1lt2nq  7207  m1p1sr  7561  m1m1sr  7562  0lt1sr  7566  axi2m1  7676  mul4i  7903  add4i  7920  addsub4i  8051  muladdi  8164  lt2addi  8265  le2addi  8266  mulap0i  8410  divap0i  8513  divmuldivapi  8525  divmul13api  8526  divadddivapi  8527  divdivdivapi  8528  subrecapi  8592  8th4div3  8932  iap0  8936  fldiv4p1lem1div2  10071  sqrt2gt1lt2  10814  abs3lemi  10922  3dvds2dec  11552  flodddiv4  11620  nprmi  11794  sinhalfpilem  12861