Theorem mpan9 281

Description: Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpan9.1	⊢ (𝜑 → 𝜓)
mpan9.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
mpan9	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mpan9

Step	Hyp	Ref	Expression
1		mpan9.1	. . 3 ⊢ (𝜑 → 𝜓)
2		mpan9.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3	1, 2	syl5 32	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 125	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used by:  sylan  283  vtocl2gf  2885  vtocl3gf  2886  vtoclegft  2897  sbcthdv  3066  disji2  4122  exmid1stab  4347  swopolem  4452  funssres  5423  fvmptssdm  5793  fmptcof  5878  fliftfuns  6007  isorel  6017  oveqrspc2v  6115  caovclg  6245  caovcomg  6248  caovassg  6251  caovcang  6254  caovordig  6258  caovordg  6260  caovdig  6267  caovdirg  6270  qliftfuns  6898  nneneq  7164  supmoti  7339  exmidonfinlem  7551  recexprlemopl  7998  recexprlemopu  8000  cauappcvgprlemladdrl  8030  caucvgsrlemcl  8162  caucvgsrlemfv  8164  caucvgsr  8175  suplocsrlempr  8180  ltordlem  8817  lble  9285  uz11  9960  seq3caopr3  10948  hashfibclem  11303  ccatass  11397  swrdswrd  11498  swrdccatin1  11518  swrdccatin2  11522  climcaucn  12141  sumdc  12148  fsum3  12178  fsumf1o  12181  fsum3cvg2  12185  isummulc2  12217  fsum2dlemstep  12225  fisumcom2  12229  fsumshftm  12236  fisum0diag2  12238  fsum00  12253  isumshft  12281  clim2prod  12330  prodmodclem2  12368  zproddc  12370  fprodseq  12374  fprodf1o  12379  prodssdc  12380  fprodm1s  12392  fprodp1s  12393  fprodcllemf  12404  fprodabs  12407  fprod2dlemstep  12413  fprodcom2fi  12417  dvdsprm  12940  pythagtriplem4  13075  pcmptdvds  13152  lidrididd  13760  grpidinv2  13921  ghmlin  14109  cntzmhm2  14173  gsumsnfdcmn  14256  idjusnfi  14269  srgrz  14394  srglz  14395  ringinvnz1ne0  14460  rrgeq0i  14680  lmodlema  14736  islmodd  14737  lsslss  14826  assalem  15111  ssnei2  15400  psmet0  15570  psmettri2  15571  cncfi  15821  dvcn  15943  dvmptfsum  15968  usgruspgrben  16649  wlk1walkdom  16822  clwwlknonex2lem2  16901  nninfsellemdc  17276