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  9701  1lt2nq  11014  m1p1sr  11133  m1m1sr  11134  axi2m1  11200  mul4i  11459  add4i  11487  add42i  11488  addsub4i  11606  muladdi  11715  lt2addi  11826  le2addi  11827  mulne0i  11907  divne0i  12016  divmuldivi  12028  divadddivi  12030  divdivdivi  12031  subreci  12099  8th4div3  12488  xrsup0  13366  fldiv4p1lem1div2  13876  sqrt2gt1lt2  15314  3dvds2dec  16371  flodddiv4  16453  nprmi  16727  mod2xnegi  17110  catcfuccl  18164  catcxpccl  18253  iccpnfhmeo  24977  xrhmeo  24978  cnheiborlem  24987  pcoval1  25047  pcoval2  25050  pcoass  25058  lhop1lem  26053  efcvx  26494  cos0pilt1  26575  dvrelog  26680  dvlog  26694  dvlog2  26696  dvsqrt  26785  dvcnsqrt  26787  cxpcn3  26792  ang180lem1  26853  dvatan  26979  log2cnv  26988  log2tlbnd  26989  log2ub  26993  harmonicbnd3  27052  ppiub  27249  bposlem8  27336  bposlem9  27337  lgsdir2lem1  27370  m1lgs  27433  2lgslem4  27451  2sqlem11  27474  2sqreultlem  27492  2sqreunnltlem  27495  chebbnd1  27517  0slt1s  27875  nohalf  28408  usgrexmplef  29277  siilem1  30871  hvadd4i  31078  his35i  31109  bdophsi  32116  bdopcoi  32118  mdcompli  32449  dmdcompli  32450  cshw1s2  32946  xrge00  33018  evl1deg3  33604  sqsscirc1  33908  raddcn  33929  xrge0iifcnv  33933  xrge0iifiso  33935  xrge0iifhom  33937  esumcvgsum  34090  dstfrvclim1  34481  signsply0  34567  cvmlift2lem6  35314  cvmlift2lem12  35320  iccioo01  37329  poimirlem9  37637  poimirlem15  37643  sqdeccom12  42329  lhe4.4ex1a  44353  dvcosre  45932  wallispi  46090  fourierdlem57  46183  fourierdlem58  46184  fourierdlem112  46238  fouriersw  46251  2exp340mod341  47725  8exp8mod9  47728  nfermltl8rev  47734  tgblthelfgott  47807  zlmodzxzequa  48418  zlmodzxzequap  48421  sepfsepc  48832