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  9581  1lt2nq  10896  m1p1sr  11015  m1m1sr  11016  axi2m1  11082  mul4i  11342  add4i  11370  add42i  11371  addsub4i  11489  muladdi  11600  lt2addi  11711  le2addi  11712  mulne0i  11792  divne0i  11901  divmuldivi  11913  divadddivi  11915  divdivdivi  11916  subreci  11984  8th4div3  12373  xrsup0  13250  fldiv4p1lem1div2  13767  sqrt2gt1lt2  15209  3dvds2dec  16272  flodddiv4  16354  nprmi  16628  mod2xnegi  17011  catcfuccl  18054  catcxpccl  18142  iccpnfhmeo  24911  xrhmeo  24912  cnheiborlem  24921  pcoval1  24981  pcoval2  24984  pcoass  24992  lhop1lem  25986  efcvx  26427  cos0pilt1  26509  dvrelog  26614  dvlog  26628  dvlog2  26630  dvsqrt  26719  dvcnsqrt  26721  cxpcn3  26726  ang180lem1  26787  dvatan  26913  log2cnv  26922  log2tlbnd  26923  log2ub  26927  harmonicbnd3  26986  ppiub  27183  bposlem8  27270  bposlem9  27271  lgsdir2lem1  27304  m1lgs  27367  2lgslem4  27385  2sqlem11  27408  2sqreultlem  27426  2sqreunnltlem  27429  chebbnd1  27451  0lt1s  27820  twocut  28431  usgrexmplef  29344  siilem1  30938  hvadd4i  31145  his35i  31176  bdophsi  32183  bdopcoi  32185  mdcompli  32516  dmdcompli  32517  cshw1s2  33052  xrge00  33106  evl1deg3  33670  cos9thpiminplylem5  33963  sqsscirc1  34085  raddcn  34106  xrge0iifcnv  34110  xrge0iifiso  34112  xrge0iifhom  34114  esumcvgsum  34265  dstfrvclim1  34655  signsply0  34728  cvmlift2lem6  35521  cvmlift2lem12  35527  iccioo01  37579  poimirlem9  37877  poimirlem15  37883  sqdeccom12  42656  lhe4.4ex1a  44682  dvcosre  46267  wallispi  46425  fourierdlem57  46518  fourierdlem58  46519  fourierdlem112  46573  fouriersw  46586  2exp340mod341  48090  8exp8mod9  48093  nfermltl8rev  48099  tgblthelfgott  48172  pgnbgreunbgrlem2lem1  48471  pgnbgreunbgrlem2lem2  48472  pgnbgreunbgrlem2lem3  48473  zlmodzxzequa  48853  zlmodzxzequap  48856  sepfsepc  49284