Theorem mp4an 692

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  noinfep  9655  1lt2nq  10968  m1p1sr  11087  m1m1sr  11088  axi2m1  11154  mul4i  11411  add4i  11438  add42i  11439  addsub4i  11556  muladdi  11665  lt2addi  11776  le2addi  11777  mulne0i  11857  divne0i  11962  divmuldivi  11974  divadddivi  11976  divdivdivi  11977  subreci  12044  8th4div3  12432  xrsup0  13302  fldiv4p1lem1div2  13800  sqrt2gt1lt2  15221  3dvds2dec  16276  flodddiv4  16356  nprmi  16626  mod2xnegi  17004  catcfuccl  18069  catcfucclOLD  18070  catcxpccl  18159  catcxpcclOLD  18160  iccpnfhmeo  24461  xrhmeo  24462  cnheiborlem  24470  pcoval1  24529  pcoval2  24532  pcoass  24540  lhop1lem  25530  efcvx  25961  cos0pilt1  26041  dvrelog  26145  dvlog  26159  dvlog2  26161  dvsqrt  26250  dvcnsqrt  26252  cxpcn3  26256  ang180lem1  26314  dvatan  26440  log2cnv  26449  log2tlbnd  26450  log2ub  26454  harmonicbnd3  26512  ppiub  26707  bposlem8  26794  bposlem9  26795  lgsdir2lem1  26828  m1lgs  26891  2lgslem4  26909  2sqlem11  26932  2sqreultlem  26950  2sqreunnltlem  26953  chebbnd1  26975  0slt1s  27330  usgrexmplef  28516  siilem1  30104  hvadd4i  30311  his35i  30342  bdophsi  31349  bdopcoi  31351  mdcompli  31682  dmdcompli  31683  cshw1s2  32124  xrge00  32187  sqsscirc1  32888  raddcn  32909  xrge0iifcnv  32913  xrge0iifiso  32915  xrge0iifhom  32917  esumcvgsum  33086  dstfrvclim1  33476  signsply0  33562  cvmlift2lem6  34299  cvmlift2lem12  34305  iccioo01  36208  poimirlem9  36497  poimirlem15  36503  sqdeccom12  41201  lhe4.4ex1a  43088  dvcosre  44628  wallispi  44786  fourierdlem57  44879  fourierdlem58  44880  fourierdlem112  44934  fouriersw  44947  2exp340mod341  46401  8exp8mod9  46404  nfermltl8rev  46410  tgblthelfgott  46483  zlmodzxzequa  47177  zlmodzxzequap  47180  sepfsepc  47560