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  9561  1lt2nq  10875  m1p1sr  10994  m1m1sr  10995  axi2m1  11061  mul4i  11321  add4i  11349  add42i  11350  addsub4i  11468  muladdi  11579  lt2addi  11690  le2addi  11691  mulne0i  11771  divne0i  11880  divmuldivi  11892  divadddivi  11894  divdivdivi  11895  subreci  11963  8th4div3  12352  xrsup0  13229  fldiv4p1lem1div2  13746  sqrt2gt1lt2  15188  3dvds2dec  16251  flodddiv4  16333  nprmi  16607  mod2xnegi  16990  catcfuccl  18033  catcxpccl  18121  iccpnfhmeo  24890  xrhmeo  24891  cnheiborlem  24900  pcoval1  24960  pcoval2  24963  pcoass  24971  lhop1lem  25965  efcvx  26406  cos0pilt1  26488  dvrelog  26593  dvlog  26607  dvlog2  26609  dvsqrt  26698  dvcnsqrt  26700  cxpcn3  26705  ang180lem1  26766  dvatan  26892  log2cnv  26901  log2tlbnd  26902  log2ub  26906  harmonicbnd3  26965  ppiub  27162  bposlem8  27249  bposlem9  27250  lgsdir2lem1  27283  m1lgs  27346  2lgslem4  27364  2sqlem11  27387  2sqreultlem  27405  2sqreunnltlem  27408  chebbnd1  27430  0slt1s  27793  twocut  28366  usgrexmplef  29258  siilem1  30852  hvadd4i  31059  his35i  31090  bdophsi  32097  bdopcoi  32099  mdcompli  32430  dmdcompli  32431  cshw1s2  32970  xrge00  33024  evl1deg3  33587  cos9thpiminplylem5  33871  sqsscirc1  33993  raddcn  34014  xrge0iifcnv  34018  xrge0iifiso  34020  xrge0iifhom  34022  esumcvgsum  34173  dstfrvclim1  34563  signsply0  34636  cvmlift2lem6  35424  cvmlift2lem12  35430  iccioo01  37444  poimirlem9  37742  poimirlem15  37748  sqdeccom12  42459  lhe4.4ex1a  44486  dvcosre  46072  wallispi  46230  fourierdlem57  46323  fourierdlem58  46324  fourierdlem112  46378  fouriersw  46391  2exp340mod341  47895  8exp8mod9  47898  nfermltl8rev  47904  tgblthelfgott  47977  pgnbgreunbgrlem2lem1  48276  pgnbgreunbgrlem2lem2  48277  pgnbgreunbgrlem2lem3  48278  zlmodzxzequa  48658  zlmodzxzequap  48661  sepfsepc  49089