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  7492  m1p1sr  7846  m1m1sr  7847  0lt1sr  7851  axi2m1  7961  mul4i  8193  add4i  8210  addsub4i  8341  muladdi  8454  lt2addi  8556  le2addi  8557  mulap0i  8702  divap0i  8806  divmuldivapi  8818  divmul13api  8819  divadddivapi  8820  divdivdivapi  8821  subrecapi  8886  8th4div3  9229  iap0  9233  fldiv4p1lem1div2  10414  sqrt2gt1lt2  11233  abs3lemi  11341  3dvds2dec  12050  flodddiv4  12120  nprmi  12319  modxai  12612  sinhalfpilem  15135  cos0pilt1  15196  lgsdir2lem1  15377  lgsdir2lem5  15381  m1lgs  15434  2lgslem4  15452