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  9639  1lt2nq  10982  m1p1sr  11101  m1m1sr  11102  axi2m1  11168  mul4i  11431  add4i  11459  add42i  11460  addsub4i  11578  muladdi  11689  lt2addi  11800  le2addi  11801  mulne0i  11881  divne0i  11987  divmuldivi  11999  divadddivi  12001  divdivdivi  12002  subreci  12070  8th4div3  12488  xrsup0  13375  fldiv4p1lem1div2  13896  sqrt2gt1lt2  15361  3dvds2dec  16423  flodddiv4  16505  nprmi  16779  mod2xnegi  17163  catcfuccl  18207  catcxpccl  18295  degenmgmopdm  19047  iccpnfhmeo  25173  xrhmeo  25174  cnheiborlem  25182  pcoval1  25241  pcoval2  25244  pcoass  25252  lhop1lem  26240  efcvx  26685  cos0pilt1  26769  dvrelog  26874  dvlog  26888  dvlog2  26890  dvsqrt  26979  dvcnsqrt  26981  cxpcn3  26985  ang180lem1  27046  dvatan  27172  log2cnv  27181  log2tlbnd  27182  log2ub  27186  harmonicbnd3  27244  ppiub  27440  bposlem8  27527  bposlem9  27528  lgsdir2lem1  27561  m1lgs  27624  2lgslem4  27642  2sqlem11  27665  2sqreultlem  27683  2sqreunnltlem  27686  chebbnd1  27708  0lt1s  28077  twocut  28688  usgrexmplef  29719  siilem1  31332  hvadd4i  31539  his35i  31570  bdophsi  32577  bdopcoi  32579  mdcompli  32910  dmdcompli  32911  cshw1s2  33400  xrge00  33454  evl1deg3  33988  cos9thpiminplylem5  34296  sqsscirc1  34418  raddcn  34439  xrge0iifcnv  34443  xrge0iifiso  34445  xrge0iifhom  34447  esumcvgsum  34598  dstfrvclim1  34989  signsply0  35059  cvmlift2lem6  35887  cvmlift2lem12  35893  iccioo01  38081  poimirlem9  38378  poimirlem15  38384  sqdeccom12  43164  lhe4.4ex1a  45153  dvcosre  46740  wallispi  46898  fourierdlem57  46991  fourierdlem58  46992  fourierdlem112  47046  fouriersw  47059  2exp340mod341  48649  8exp8mod9  48652  nfermltl8rev  48658  tgblthelfgott  48731  pgnbgreunbgrlem2lem1  49030  pgnbgreunbgrlem2lem2  49031  pgnbgreunbgrlem2lem3  49032  zlmodzxzequa  49426  zlmodzxzequap  49429  sepfsepc  49854