Theorem mp4an 680

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  noinfep  8919  1lt2nq  10195  m1p1sr  10314  m1m1sr  10315  axi2m1  10381  mul4i  10639  add4i  10666  add42i  10667  addsub4i  10785  muladdi  10894  lt2addi  11005  le2addi  11006  mulne0i  11086  divne0i  11191  divmuldivi  11203  divadddivi  11205  divdivdivi  11206  subreci  11273  8th4div3  11670  xrsup0  12535  fldiv4p1lem1div2  13023  sqrt2gt1lt2  14498  3dvds2dec  15545  flodddiv4  15627  nprmi  15892  mod2xnegi  16266  catcfuccl  17230  catcxpccl  17318  iccpnfhmeo  23255  xrhmeo  23256  cnheiborlem  23264  pcoval1  23323  pcoval2  23326  pcoass  23334  lhop1lem  24316  efcvx  24743  dvrelog  24924  dvlog  24938  dvlog2  24940  dvsqrt  25027  dvcnsqrt  25029  cxpcn3  25033  ang180lem1  25091  dvatan  25217  log2cnv  25227  log2tlbnd  25228  log2ub  25232  harmonicbnd3  25290  ppiub  25485  bposlem8  25572  bposlem9  25573  lgsdir2lem1  25606  m1lgs  25669  2lgslem4  25687  2sqlem11  25710  2sqreultlem  25728  2sqreunnltlem  25731  chebbnd1  25753  usgrexmplef  26747  siilem1  28408  hvadd4i  28617  his35i  28648  bdophsi  29657  bdopcoi  29659  mdcompli  29990  dmdcompli  29991  xrge00  30405  sqsscirc1  30795  raddcn  30816  xrge0iifcnv  30820  xrge0iifiso  30822  xrge0iifhom  30824  esumcvgsum  30991  dstfrvclim1  31381  signsply0  31467  cvmlift2lem6  32140  cvmlift2lem12  32146  poimirlem9  34342  poimirlem15  34348  sqdeccom12  38607  lhe4.4ex1a  40077  dvcosre  41627  wallispi  41787  fourierdlem57  41880  fourierdlem58  41881  fourierdlem112  41935  fouriersw  41948  2exp340mod341  43267  8exp8mod9  43270  nfermltl8rev  43276  tgblthelfgott  43349  zlmodzxzequa  43919  zlmodzxzequap  43922