Theorem mp4an 689

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 688	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 206  df-an 396

This theorem is referenced by:  noinfep  9348  1lt2nq  10660  m1p1sr  10779  m1m1sr  10780  axi2m1  10846  mul4i  11102  add4i  11129  add42i  11130  addsub4i  11247  muladdi  11356  lt2addi  11467  le2addi  11468  mulne0i  11548  divne0i  11653  divmuldivi  11665  divadddivi  11667  divdivdivi  11668  subreci  11735  8th4div3  12123  xrsup0  12986  fldiv4p1lem1div2  13483  sqrt2gt1lt2  14914  3dvds2dec  15970  flodddiv4  16050  nprmi  16322  mod2xnegi  16700  catcfuccl  17750  catcfucclOLD  17751  catcxpccl  17840  catcxpcclOLD  17841  iccpnfhmeo  24014  xrhmeo  24015  cnheiborlem  24023  pcoval1  24082  pcoval2  24085  pcoass  24093  lhop1lem  25082  efcvx  25513  cos0pilt1  25593  dvrelog  25697  dvlog  25711  dvlog2  25713  dvsqrt  25800  dvcnsqrt  25802  cxpcn3  25806  ang180lem1  25864  dvatan  25990  log2cnv  25999  log2tlbnd  26000  log2ub  26004  harmonicbnd3  26062  ppiub  26257  bposlem8  26344  bposlem9  26345  lgsdir2lem1  26378  m1lgs  26441  2lgslem4  26459  2sqlem11  26482  2sqreultlem  26500  2sqreunnltlem  26503  chebbnd1  26525  usgrexmplef  27529  siilem1  29114  hvadd4i  29321  his35i  29352  bdophsi  30359  bdopcoi  30361  mdcompli  30692  dmdcompli  30693  cshw1s2  31134  xrge00  31197  sqsscirc1  31760  raddcn  31781  xrge0iifcnv  31785  xrge0iifiso  31787  xrge0iifhom  31789  esumcvgsum  31956  dstfrvclim1  32344  signsply0  32430  cvmlift2lem6  33170  cvmlift2lem12  33176  0slt1s  33950  iccioo01  35425  poimirlem9  35713  poimirlem15  35719  sqdeccom12  40238  lhe4.4ex1a  41836  dvcosre  43343  wallispi  43501  fourierdlem57  43594  fourierdlem58  43595  fourierdlem112  43649  fouriersw  43662  2exp340mod341  45073  8exp8mod9  45076  nfermltl8rev  45082  tgblthelfgott  45155  zlmodzxzequa  45725  zlmodzxzequap  45728  sepfsepc  46109