Theorem mp4an 693

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 692	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  9545  1lt2nq  10859  m1p1sr  10978  m1m1sr  10979  axi2m1  11045  mul4i  11305  add4i  11333  add42i  11334  addsub4i  11452  muladdi  11563  lt2addi  11674  le2addi  11675  mulne0i  11755  divne0i  11864  divmuldivi  11876  divadddivi  11878  divdivdivi  11879  subreci  11947  8th4div3  12336  xrsup0  13217  fldiv4p1lem1div2  13734  sqrt2gt1lt2  15176  3dvds2dec  16239  flodddiv4  16321  nprmi  16595  mod2xnegi  16978  catcfuccl  18020  catcxpccl  18108  iccpnfhmeo  24865  xrhmeo  24866  cnheiborlem  24875  pcoval1  24935  pcoval2  24938  pcoass  24946  lhop1lem  25940  efcvx  26381  cos0pilt1  26463  dvrelog  26568  dvlog  26582  dvlog2  26584  dvsqrt  26673  dvcnsqrt  26675  cxpcn3  26680  ang180lem1  26741  dvatan  26867  log2cnv  26876  log2tlbnd  26877  log2ub  26881  harmonicbnd3  26940  ppiub  27137  bposlem8  27224  bposlem9  27225  lgsdir2lem1  27258  m1lgs  27321  2lgslem4  27339  2sqlem11  27362  2sqreultlem  27380  2sqreunnltlem  27383  chebbnd1  27405  0slt1s  27768  twocut  28341  usgrexmplef  29232  siilem1  30823  hvadd4i  31030  his35i  31061  bdophsi  32068  bdopcoi  32070  mdcompli  32401  dmdcompli  32402  cshw1s2  32933  xrge00  32987  evl1deg3  33533  cos9thpiminplylem5  33791  sqsscirc1  33913  raddcn  33934  xrge0iifcnv  33938  xrge0iifiso  33940  xrge0iifhom  33942  esumcvgsum  34093  dstfrvclim1  34483  signsply0  34556  cvmlift2lem6  35344  cvmlift2lem12  35350  iccioo01  37361  poimirlem9  37669  poimirlem15  37675  sqdeccom12  42322  lhe4.4ex1a  44362  dvcosre  45950  wallispi  46108  fourierdlem57  46201  fourierdlem58  46202  fourierdlem112  46256  fouriersw  46269  2exp340mod341  47764  8exp8mod9  47767  nfermltl8rev  47773  tgblthelfgott  47846  pgnbgreunbgrlem2lem1  48145  pgnbgreunbgrlem2lem2  48146  pgnbgreunbgrlem2lem3  48147  zlmodzxzequa  48528  zlmodzxzequap  48531  sepfsepc  48959