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  9575  1lt2nq  10886  m1p1sr  11005  m1m1sr  11006  axi2m1  11072  mul4i  11331  add4i  11359  add42i  11360  addsub4i  11478  muladdi  11589  lt2addi  11700  le2addi  11701  mulne0i  11781  divne0i  11890  divmuldivi  11902  divadddivi  11904  divdivdivi  11905  subreci  11973  8th4div3  12362  xrsup0  13243  fldiv4p1lem1div2  13757  sqrt2gt1lt2  15199  3dvds2dec  16262  flodddiv4  16344  nprmi  16618  mod2xnegi  17001  catcfuccl  18043  catcxpccl  18131  iccpnfhmeo  24859  xrhmeo  24860  cnheiborlem  24869  pcoval1  24929  pcoval2  24932  pcoass  24940  lhop1lem  25934  efcvx  26375  cos0pilt1  26457  dvrelog  26562  dvlog  26576  dvlog2  26578  dvsqrt  26667  dvcnsqrt  26669  cxpcn3  26674  ang180lem1  26735  dvatan  26861  log2cnv  26870  log2tlbnd  26871  log2ub  26875  harmonicbnd3  26934  ppiub  27131  bposlem8  27218  bposlem9  27219  lgsdir2lem1  27252  m1lgs  27315  2lgslem4  27333  2sqlem11  27356  2sqreultlem  27374  2sqreunnltlem  27377  chebbnd1  27399  0slt1s  27761  twocut  28333  usgrexmplef  29222  siilem1  30813  hvadd4i  31020  his35i  31051  bdophsi  32058  bdopcoi  32060  mdcompli  32391  dmdcompli  32392  cshw1s2  32915  xrge00  32981  evl1deg3  33526  cos9thpiminplylem5  33755  sqsscirc1  33877  raddcn  33898  xrge0iifcnv  33902  xrge0iifiso  33904  xrge0iifhom  33906  esumcvgsum  34057  dstfrvclim1  34448  signsply0  34521  cvmlift2lem6  35283  cvmlift2lem12  35289  iccioo01  37303  poimirlem9  37611  poimirlem15  37617  sqdeccom12  42265  lhe4.4ex1a  44305  dvcosre  45897  wallispi  46055  fourierdlem57  46148  fourierdlem58  46149  fourierdlem112  46203  fouriersw  46216  2exp340mod341  47721  8exp8mod9  47724  nfermltl8rev  47730  tgblthelfgott  47803  pgnbgreunbgrlem2lem1  48102  pgnbgreunbgrlem2lem2  48103  pgnbgreunbgrlem2lem3  48104  zlmodzxzequa  48485  zlmodzxzequap  48488  sepfsepc  48916