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  9698  1lt2nq  11011  m1p1sr  11130  m1m1sr  11131  axi2m1  11197  mul4i  11456  add4i  11484  add42i  11485  addsub4i  11603  muladdi  11712  lt2addi  11823  le2addi  11824  mulne0i  11904  divne0i  12013  divmuldivi  12025  divadddivi  12027  divdivdivi  12028  subreci  12095  8th4div3  12484  xrsup0  13362  fldiv4p1lem1div2  13872  sqrt2gt1lt2  15310  3dvds2dec  16367  flodddiv4  16449  nprmi  16723  mod2xnegi  17105  catcfuccl  18173  catcfucclOLD  18174  catcxpccl  18263  catcxpcclOLD  18264  iccpnfhmeo  24990  xrhmeo  24991  cnheiborlem  25000  pcoval1  25060  pcoval2  25063  pcoass  25071  lhop1lem  26067  efcvx  26508  cos0pilt1  26589  dvrelog  26694  dvlog  26708  dvlog2  26710  dvsqrt  26799  dvcnsqrt  26801  cxpcn3  26806  ang180lem1  26867  dvatan  26993  log2cnv  27002  log2tlbnd  27003  log2ub  27007  harmonicbnd3  27066  ppiub  27263  bposlem8  27350  bposlem9  27351  lgsdir2lem1  27384  m1lgs  27447  2lgslem4  27465  2sqlem11  27488  2sqreultlem  27506  2sqreunnltlem  27509  chebbnd1  27531  0slt1s  27889  nohalf  28422  usgrexmplef  29291  siilem1  30880  hvadd4i  31087  his35i  31118  bdophsi  32125  bdopcoi  32127  mdcompli  32458  dmdcompli  32459  cshw1s2  32930  xrge00  33000  evl1deg3  33583  sqsscirc1  33869  raddcn  33890  xrge0iifcnv  33894  xrge0iifiso  33896  xrge0iifhom  33898  esumcvgsum  34069  dstfrvclim1  34459  signsply0  34545  cvmlift2lem6  35293  cvmlift2lem12  35299  iccioo01  37310  poimirlem9  37616  poimirlem15  37622  sqdeccom12  42303  lhe4.4ex1a  44325  dvcosre  45868  wallispi  46026  fourierdlem57  46119  fourierdlem58  46120  fourierdlem112  46174  fouriersw  46187  2exp340mod341  47658  8exp8mod9  47661  nfermltl8rev  47667  tgblthelfgott  47740  zlmodzxzequa  48342  zlmodzxzequap  48345  sepfsepc  48724