Theorem mp4an 699

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  noinfep  9572  1lt2nq  10887  m1p1sr  11006  m1m1sr  11007  axi2m1  11073  mul4i  11334  add4i  11362  add42i  11363  addsub4i  11481  muladdi  11592  lt2addi  11703  le2addi  11704  mulne0i  11784  divne0i  11894  divmuldivi  11906  divadddivi  11908  divdivdivi  11909  subreci  11977  8th4div3  12388  xrsup0  13266  fldiv4p1lem1div2  13785  sqrt2gt1lt2  15227  3dvds2dec  16293  flodddiv4  16375  nprmi  16649  mod2xnegi  17033  catcfuccl  18076  catcxpccl  18164  iccpnfhmeo  24930  xrhmeo  24931  cnheiborlem  24939  pcoval1  24998  pcoval2  25001  pcoass  25009  lhop1lem  25998  efcvx  26432  cos0pilt1  26514  dvrelog  26619  dvlog  26633  dvlog2  26635  dvsqrt  26724  dvcnsqrt  26726  cxpcn3  26730  ang180lem1  26791  dvatan  26917  log2cnv  26926  log2tlbnd  26927  log2ub  26931  harmonicbnd3  26989  ppiub  27185  bposlem8  27272  bposlem9  27273  lgsdir2lem1  27306  m1lgs  27369  2lgslem4  27387  2sqlem11  27410  2sqreultlem  27428  2sqreunnltlem  27431  chebbnd1  27453  0lt1s  27822  twocut  28433  usgrexmplef  29346  siilem1  30940  hvadd4i  31147  his35i  31178  bdophsi  32185  bdopcoi  32187  mdcompli  32518  dmdcompli  32519  cshw1s2  33039  xrge00  33093  evl1deg3  33661  cos9thpiminplylem5  33970  sqsscirc1  34092  raddcn  34113  xrge0iifcnv  34117  xrge0iifiso  34119  xrge0iifhom  34121  esumcvgsum  34272  dstfrvclim1  34662  signsply0  34735  cvmlift2lem6  35536  cvmlift2lem12  35542  iccioo01  37689  poimirlem9  37996  poimirlem15  38002  sqdeccom12  42766  lhe4.4ex1a  44773  dvcosre  46355  wallispi  46513  fourierdlem57  46606  fourierdlem58  46607  fourierdlem112  46661  fouriersw  46674  2exp340mod341  48224  8exp8mod9  48227  nfermltl8rev  48233  tgblthelfgott  48306  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  zlmodzxzequa  48987  zlmodzxzequap  48990  sepfsepc  49418