Theorem mp4an 692

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 691	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  9729  1lt2nq  11042  m1p1sr  11161  m1m1sr  11162  axi2m1  11228  mul4i  11487  add4i  11514  add42i  11515  addsub4i  11632  muladdi  11741  lt2addi  11852  le2addi  11853  mulne0i  11933  divne0i  12042  divmuldivi  12054  divadddivi  12056  divdivdivi  12057  subreci  12124  8th4div3  12513  xrsup0  13385  fldiv4p1lem1div2  13886  sqrt2gt1lt2  15323  3dvds2dec  16381  flodddiv4  16461  nprmi  16736  mod2xnegi  17118  catcfuccl  18186  catcfucclOLD  18187  catcxpccl  18276  catcxpcclOLD  18277  iccpnfhmeo  24995  xrhmeo  24996  cnheiborlem  25005  pcoval1  25065  pcoval2  25068  pcoass  25076  lhop1lem  26072  efcvx  26511  cos0pilt1  26592  dvrelog  26697  dvlog  26711  dvlog2  26713  dvsqrt  26802  dvcnsqrt  26804  cxpcn3  26809  ang180lem1  26870  dvatan  26996  log2cnv  27005  log2tlbnd  27006  log2ub  27010  harmonicbnd3  27069  ppiub  27266  bposlem8  27353  bposlem9  27354  lgsdir2lem1  27387  m1lgs  27450  2lgslem4  27468  2sqlem11  27491  2sqreultlem  27509  2sqreunnltlem  27512  chebbnd1  27534  0slt1s  27892  nohalf  28425  usgrexmplef  29294  siilem1  30883  hvadd4i  31090  his35i  31121  bdophsi  32128  bdopcoi  32130  mdcompli  32461  dmdcompli  32462  cshw1s2  32927  xrge00  32998  evl1deg3  33568  sqsscirc1  33854  raddcn  33875  xrge0iifcnv  33879  xrge0iifiso  33881  xrge0iifhom  33883  esumcvgsum  34052  dstfrvclim1  34442  signsply0  34528  cvmlift2lem6  35276  cvmlift2lem12  35282  iccioo01  37293  poimirlem9  37589  poimirlem15  37595  sqdeccom12  42278  lhe4.4ex1a  44298  dvcosre  45833  wallispi  45991  fourierdlem57  46084  fourierdlem58  46085  fourierdlem112  46139  fouriersw  46152  2exp340mod341  47607  8exp8mod9  47610  nfermltl8rev  47616  tgblthelfgott  47689  zlmodzxzequa  48225  zlmodzxzequap  48228  sepfsepc  48607