Theorem mp4an 694

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

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  noinfep  9572  1lt2nq  10887  m1p1sr  11006  m1m1sr  11007  axi2m1  11073  mul4i  11334  add4i  11362  add42i  11363  addsub4i  11481  muladdi  11592  lt2addi  11703  le2addi  11704  mulne0i  11784  divne0i  11894  divmuldivi  11906  divadddivi  11908  divdivdivi  11909  subreci  11977  8th4div3  12388  xrsup0  13266  fldiv4p1lem1div2  13785  sqrt2gt1lt2  15227  3dvds2dec  16293  flodddiv4  16375  nprmi  16649  mod2xnegi  17033  catcfuccl  18076  catcxpccl  18164  iccpnfhmeo  24922  xrhmeo  24923  cnheiborlem  24931  pcoval1  24990  pcoval2  24993  pcoass  25001  lhop1lem  25990  efcvx  26427  cos0pilt1  26509  dvrelog  26614  dvlog  26628  dvlog2  26630  dvsqrt  26719  dvcnsqrt  26721  cxpcn3  26725  ang180lem1  26786  dvatan  26912  log2cnv  26921  log2tlbnd  26922  log2ub  26926  harmonicbnd3  26985  ppiub  27181  bposlem8  27268  bposlem9  27269  lgsdir2lem1  27302  m1lgs  27365  2lgslem4  27383  2sqlem11  27406  2sqreultlem  27424  2sqreunnltlem  27427  chebbnd1  27449  0lt1s  27818  twocut  28429  usgrexmplef  29342  siilem1  30937  hvadd4i  31144  his35i  31175  bdophsi  32182  bdopcoi  32184  mdcompli  32515  dmdcompli  32516  cshw1s2  33035  xrge00  33089  evl1deg3  33653  cos9thpiminplylem5  33946  sqsscirc1  34068  raddcn  34089  xrge0iifcnv  34093  xrge0iifiso  34095  xrge0iifhom  34097  esumcvgsum  34248  dstfrvclim1  34638  signsply0  34711  cvmlift2lem6  35506  cvmlift2lem12  35512  iccioo01  37657  poimirlem9  37964  poimirlem15  37970  sqdeccom12  42735  lhe4.4ex1a  44774  dvcosre  46358  wallispi  46516  fourierdlem57  46609  fourierdlem58  46610  fourierdlem112  46664  fouriersw  46677  2exp340mod341  48221  8exp8mod9  48224  nfermltl8rev  48230  tgblthelfgott  48303  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  pgnbgreunbgrlem2lem3  48604  zlmodzxzequa  48984  zlmodzxzequap  48987  sepfsepc  49415