Theorem mp4an 706

Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010.)

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  noinfep  9643  1lt2nq  10986  m1p1sr  11105  m1m1sr  11106  axi2m1  11172  mul4i  11435  add4i  11463  add42i  11464  addsub4i  11582  muladdi  11693  lt2addi  11804  le2addi  11805  mulne0i  11885  divne0i  11991  divmuldivi  12003  divadddivi  12005  divdivdivi  12006  subreci  12074  8th4div3  12492  xrsup0  13379  fldiv4p1lem1div2  13900  sqrt2gt1lt2  15365  3dvds2dec  16429  flodddiv4  16511  nprmi  16785  mod2xnegi  17169  catcfuccl  18213  catcxpccl  18301  degenmgmopdm  19053  iccpnfhmeo  25179  xrhmeo  25180  cnheiborlem  25188  pcoval1  25247  pcoval2  25250  pcoass  25258  lhop1lem  26247  efcvx  26692  cos0pilt1  26777  dvrelog  26882  dvlog  26896  dvlog2  26898  dvsqrt  26987  dvcnsqrt  26989  cxpcn3  26993  ang180lem1  27054  dvatan  27180  log2cnv  27189  log2tlbnd  27190  log2ub  27194  harmonicbnd3  27252  ppiub  27448  bposlem8  27535  bposlem9  27536  lgsdir2lem1  27569  m1lgs  27632  2lgslem4  27650  2sqlem11  27673  2sqreultlem  27691  2sqreunnltlem  27694  chebbnd1  27716  0lt1s  28085  twocut  28696  usgrexmplef  29727  siilem1  31340  hvadd4i  31547  his35i  31578  bdophsi  32585  bdopcoi  32587  mdcompli  32918  dmdcompli  32919  cshw1s2  33408  xrge00  33462  evl1deg3  33996  cos9thpiminplylem5  34304  sqsscirc1  34426  raddcn  34447  xrge0iifcnv  34451  xrge0iifiso  34453  xrge0iifhom  34455  esumcvgsum  34606  dstfrvclim1  34997  signsply0  35067  cvmlift2lem6  35895  cvmlift2lem12  35901  iccioo01  38089  poimirlem9  38386  poimirlem15  38392  sqdeccom12  43172  lhe4.4ex1a  45161  dvcosre  46748  wallispi  46906  fourierdlem57  46999  fourierdlem58  47000  fourierdlem112  47054  fouriersw  47067  2exp340mod341  48657  8exp8mod9  48660  nfermltl8rev  48666  tgblthelfgott  48739  pgnbgreunbgrlem2lem1  49038  pgnbgreunbgrlem2lem2  49039  pgnbgreunbgrlem2lem3  49040  zlmodzxzequa  49434  zlmodzxzequap  49437  sepfsepc  49862