Theorem mp4an 706

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  noinfep  9632  1lt2nq  10969  m1p1sr  11088  m1m1sr  11089  axi2m1  11155  mul4i  11418  add4i  11446  add42i  11447  addsub4i  11565  muladdi  11676  lt2addi  11787  le2addi  11788  mulne0i  11868  divne0i  11974  divmuldivi  11986  divadddivi  11988  divdivdivi  11989  subreci  12057  8th4div3  12475  xrsup0  13360  fldiv4p1lem1div2  13881  sqrt2gt1lt2  15344  3dvds2dec  16408  flodddiv4  16490  nprmi  16764  mod2xnegi  17148  catcfuccl  18192  catcxpccl  18280  iccpnfhmeo  25133  xrhmeo  25134  cnheiborlem  25142  pcoval1  25201  pcoval2  25204  pcoass  25212  lhop1lem  26201  efcvx  26641  cos0pilt1  26726  dvrelog  26831  dvlog  26845  dvlog2  26847  dvsqrt  26936  dvcnsqrt  26938  cxpcn3  26942  ang180lem1  27003  dvatan  27129  log2cnv  27138  log2tlbnd  27139  log2ub  27143  harmonicbnd3  27201  ppiub  27397  bposlem8  27484  bposlem9  27485  lgsdir2lem1  27518  m1lgs  27581  2lgslem4  27599  2sqlem11  27622  2sqreultlem  27640  2sqreunnltlem  27643  chebbnd1  27665  0lt1s  28034  twocut  28645  usgrexmplef  29638  siilem1  31232  hvadd4i  31439  his35i  31470  bdophsi  32477  bdopcoi  32479  mdcompli  32810  dmdcompli  32811  cshw1s2  33303  xrge00  33357  evl1deg3  33891  cos9thpiminplylem5  34199  sqsscirc1  34321  raddcn  34342  xrge0iifcnv  34346  xrge0iifiso  34348  xrge0iifhom  34350  esumcvgsum  34501  dstfrvclim1  34892  signsply0  34962  cvmlift2lem6  35813  cvmlift2lem12  35819  iccioo01  38006  poimirlem9  38313  poimirlem15  38319  sqdeccom12  43083  lhe4.4ex1a  45072  dvcosre  46659  wallispi  46817  fourierdlem57  46910  fourierdlem58  46911  fourierdlem112  46965  fouriersw  46978  2exp340mod341  48531  8exp8mod9  48534  nfermltl8rev  48540  tgblthelfgott  48613  pgnbgreunbgrlem2lem1  48912  pgnbgreunbgrlem2lem2  48913  pgnbgreunbgrlem2lem3  48914  zlmodzxzequa  49309  zlmodzxzequap  49312  sepfsepc  49739  crossp3i  50682